From ae498bebaac9b7648a8f403305e8f36be5e026d8 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cohen@crans.org>
Date: Mon, 15 Feb 2021 19:39:54 +0100
Subject: [PATCH 1/3] Adding NES.Snapshot

---
 apps/NES/elpi/nes.elpi        |  5 +++++
 apps/NES/examples/usage_NES.v | 12 ++++++++++++
 apps/NES/theories/NES.v       | 12 ++++++++++++
 3 files changed, 29 insertions(+)

diff --git a/apps/NES/elpi/nes.elpi b/apps/NES/elpi/nes.elpi
index 9f611e004..70b35db3c 100644
--- a/apps/NES/elpi/nes.elpi
+++ b/apps/NES/elpi/nes.elpi
@@ -120,4 +120,9 @@ open-super-path [P|PS] ACC :-
   open-path Cur,
   open-super-path PS Cur.
 
+pred snapshot i:list string.
+snapshot Path :- std.do! [
+  std.map {std.findall (ns Path M_)} nes.ns->modpath Mods,
+  std.forall Mods coq.env.export-module
+].
 }
\ No newline at end of file
diff --git a/apps/NES/examples/usage_NES.v b/apps/NES/examples/usage_NES.v
index c3714c8cc..3289161a6 100644
--- a/apps/NES/examples/usage_NES.v
+++ b/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 Snapshot *)
+(* this allows to take a "snapshot" of a namespace at
+a given time in order to reuse it without using NES *)
+Module Snapshot.
+NES.Snapshot This.Is.A.Long.Namespace.
+End Snapshot.
+
+Section TestSnapshot.
+Import Snapshot.
+Check stuff.
+End TestSnapshot.
diff --git a/apps/NES/theories/NES.v b/apps/NES/theories/NES.v
index 959bb7467..3973a6dd4 100644
--- a/apps/NES/theories/NES.v
+++ b/apps/NES/theories/NES.v
@@ -64,3 +64,15 @@ Elpi Accumulate lp:{{
 }}.
 Elpi Typecheck.
 Elpi Export NES.Open.
+
+Elpi Command NES.Snapshot.
+Elpi Accumulate Db NES.db.
+Elpi Accumulate File "elpi/nes.elpi".
+Elpi Accumulate lp:{{
+
+  main [str NS] :- !, nes.snapshot {nes.string->ns NS}.
+  main _ :- coq.error "usage: NES.Snapshot <DotSeparatedPath>".
+
+}}.
+Elpi Typecheck.
+Elpi Export NES.Snapshot.

From f7d22ae19f09f107f09add000567583b1b5d63f4 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <cohen@crans.org>
Date: Mon, 15 Feb 2021 20:38:58 +0100
Subject: [PATCH 2/3] snapshot -> export

---
 apps/NES/elpi/nes.elpi        |  4 ++--
 apps/NES/examples/usage_NES.v | 16 ++++++++--------
 apps/NES/theories/NES.v       |  8 ++++----
 3 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/apps/NES/elpi/nes.elpi b/apps/NES/elpi/nes.elpi
index 70b35db3c..db913414c 100644
--- a/apps/NES/elpi/nes.elpi
+++ b/apps/NES/elpi/nes.elpi
@@ -120,8 +120,8 @@ open-super-path [P|PS] ACC :-
   open-path Cur,
   open-super-path PS Cur.
 
-pred snapshot i:list string.
-snapshot Path :- std.do! [
+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
 ].
diff --git a/apps/NES/examples/usage_NES.v b/apps/NES/examples/usage_NES.v
index 3289161a6..adafcf30e 100644
--- a/apps/NES/examples/usage_NES.v
+++ b/apps/NES/examples/usage_NES.v
@@ -44,14 +44,14 @@ 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 Snapshot *)
-(* this allows to take a "snapshot" of a namespace at
+(* NES Export *)
+(* this allows to take a "export" of a namespace at
 a given time in order to reuse it without using NES *)
-Module Snapshot.
-NES.Snapshot This.Is.A.Long.Namespace.
-End Snapshot.
+Module Export.
+NES.Export This.Is.A.Long.Namespace.
+End Export.
 
-Section TestSnapshot.
-Import Snapshot.
+Section TestExport.
+Import Export.
 Check stuff.
-End TestSnapshot.
+End TestExport.
diff --git a/apps/NES/theories/NES.v b/apps/NES/theories/NES.v
index 3973a6dd4..ed8349207 100644
--- a/apps/NES/theories/NES.v
+++ b/apps/NES/theories/NES.v
@@ -65,14 +65,14 @@ Elpi Accumulate lp:{{
 Elpi Typecheck.
 Elpi Export NES.Open.
 
-Elpi Command NES.Snapshot.
+Elpi Command NES.Export.
 Elpi Accumulate Db NES.db.
 Elpi Accumulate File "elpi/nes.elpi".
 Elpi Accumulate lp:{{
 
-  main [str NS] :- !, nes.snapshot {nes.string->ns NS}.
-  main _ :- coq.error "usage: NES.Snapshot <DotSeparatedPath>".
+  main [str NS] :- !, nes.export {nes.string->ns NS}.
+  main _ :- coq.error "usage: NES.Export <DotSeparatedPath>".
 
 }}.
 Elpi Typecheck.
-Elpi Export NES.Snapshot.
+Elpi Export NES.Export.

From 3af1aa66eb33b1dc41a8bf13cf3612aa08d7c072 Mon Sep 17 00:00:00 2001
From: Cyril Cohen <CohenCyril@users.noreply.github.com>
Date: Mon, 15 Feb 2021 20:45:28 +0100
Subject: [PATCH 3/3] Update comment

---
 apps/NES/examples/usage_NES.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/apps/NES/examples/usage_NES.v b/apps/NES/examples/usage_NES.v
index adafcf30e..a5085a026 100644
--- a/apps/NES/examples/usage_NES.v
+++ b/apps/NES/examples/usage_NES.v
@@ -45,7 +45,7 @@ Fail Check @default _ : nat.
    a module: if it is a namespace some "actions" have to be propagated upward *)
 
 (* NES Export *)
-(* this allows to take a "export" of a namespace at
+(* 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.