Adding NES.Export

apps/NES/elpi/nes.elpi

@@ -120,4 +120,9 @@ open-super-path [P|PS] ACC :-
   open-path Cur,
   open-super-path PS Cur.
 
+pred export i:list string.
+export Path :- std.do! [
+  std.map {std.findall (ns Path M_)} nes.ns->modpath Mods,
+  std.forall Mods coq.env.export-module
+].
 }

apps/NES/examples/usage_NES.v

@@ -43,3 +43,15 @@ Fail Check nat_def.
 Fail Check @default _ : nat.
 (* This behavior requires Libobject to be aware of the role played by
    a module: if it is a namespace some "actions" have to be propagated upward *)
+
+(* NES Export *)
+(* this allows to take a "snapshot" of a namespace at
+a given time in order to reuse it without using NES *)
+Module Export.
+NES.Export This.Is.A.Long.Namespace.
+End Export.
+
+Section TestExport.
+Import Export.
+Check stuff.
+End TestExport.

apps/NES/theories/NES.v

@@ -64,3 +64,15 @@ Elpi Accumulate lp:{{
 }}.
 Elpi Typecheck.
 Elpi Export NES.Open.
+
+Elpi Command NES.Export.
+Elpi Accumulate Db NES.db.
+Elpi Accumulate File "elpi/nes.elpi".
+Elpi Accumulate lp:{{
+
+  main [str NS] :- !, nes.export {nes.string->ns NS}.
+  main _ :- coq.error "usage: NES.Export <DotSeparatedPath>".
+
+}}.
+Elpi Typecheck.
+Elpi Export NES.Export.