Merge PR #9129: [proof] Removal of imperative state ; interpretation layers only.

Ack-by: SkySkimmer
Reviewed-by: aspiwack
Ack-by: ejgallego
Ack-by: gares
Ack-by: herbelin
Reviewed-by: mattam82
Ack-by: maximedenes

2 files changed, 35 insertions, 6 deletions

diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 73a2b99434..baa4ae0306 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -35,8 +35,23 @@ ARGUMENT EXTEND numnotoption
 END
 
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
-  | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
+  | #[ locality = Attributes.locality; ] ![proof][ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
       ident(sc) numnotoption(o) ] ->
-    { let (sigma, env) = Pfedit.get_current_context () in
-      vernac_numeral_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
+
+    { (* It is a bug to use the proof context here, but at the request of
+       * the reviewers we keep this broken behavior for now. The Global env
+       * should be used instead, and the `env, sigma` parameteter to the
+       * numeral notation command removed.
+       *)
+      fun ~pstate ->
+        let sigma, env = match pstate with
+        | None ->
+          let env = Global.env () in
+          let sigma = Evd.from_env env in
+          sigma, env
+        | Some pstate ->
+          Pfedit.get_current_context pstate
+        in
+      vernac_numeral_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) o;
+      pstate }
 END
diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg
index 171e0e213d..cc8c13a84b 100644
--- a/plugins/syntax/g_string.mlg
+++ b/plugins/syntax/g_string.mlg
@@ -19,8 +19,22 @@ open Stdarg
 }
 
 VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF
-  | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
+  | #[ locality = Attributes.locality; ] ![proof] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
       ident(sc) ] ->
-    { let (sigma, env) = Pfedit.get_current_context () in
-      vernac_string_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc) }
+    { (* It is a bug to use the proof context here, but at the request of
+       * the reviewers we keep this broken behavior for now. The Global env
+       * should be used instead, and the `env, sigma` parameteter to the
+       * numeral notation command removed.
+       *)
+      fun ~pstate ->
+        let sigma, env = match pstate with
+        | None ->
+          let env = Global.env () in
+          let sigma = Evd.from_env env in
+          sigma, env
+        | Some pstate ->
+          Pfedit.get_current_context pstate
+        in
+      vernac_string_notation env sigma (Locality.make_module_locality locality) ty f g (Id.to_string sc);
+      pstate }
 END