6 files changed, 12 insertions, 38 deletions
diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 0f0f3953da..5808385723 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -34,23 +34,8 @@ VERNAC ARGUMENT EXTEND numnotoption
 END
 
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
-  | #[ locality = Attributes.locality; ] ![proof][ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
+  | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
       ident(sc) numnotoption(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 }
+    { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
 END
diff --git a/plugins/syntax/g_string.mlg b/plugins/syntax/g_string.mlg
index cc8c13a84b..1e06cd8ddb 100644
--- a/plugins/syntax/g_string.mlg
+++ b/plugins/syntax/g_string.mlg
@@ -19,22 +19,7 @@ open Stdarg
 }
 
 VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF
-  | #[ locality = Attributes.locality; ] ![proof] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
+  | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
       ident(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 }
+    { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) }
 END
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index ec8c2338fb..b0b6fa69bb 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -101,7 +101,9 @@ let type_error_of g ty =
      str " to Decimal.int or (option Decimal.int)." ++ fnl () ++
      str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).")
 
-let vernac_numeral_notation env sigma local ty f g scope opts =
+let vernac_numeral_notation local ty f g scope opts =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
   let dec_ty = locate_decimal () in
   let z_pos_ty = locate_z () in
   let int63_ty = locate_int63 () in
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index b14ed18497..3fc0385f5d 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -14,6 +14,6 @@ open Notation
 
 (** * Numeral notation *)
 
-val vernac_numeral_notation : Environ.env -> Evd.evar_map -> locality_flag ->
+val vernac_numeral_notation : locality_flag ->
                               qualid -> qualid -> qualid ->
                               Notation_term.scope_name -> numnot_option -> unit
diff --git a/plugins/syntax/string_notation.ml b/plugins/syntax/string_notation.ml
index 5fae696d58..4234cee1bd 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -47,7 +47,9 @@ let type_error_of g ty =
     (pr_qualid g ++ str " should go from " ++ pr_qualid ty ++
      str " to Byte.byte or (option Byte.byte) or (list Byte.byte) or (option (list Byte.byte)).")
 
-let vernac_string_notation env sigma local ty f g scope =
+let vernac_string_notation local ty f g scope =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
   let app x y = mkAppC (x,[y]) in
   let cref q = mkRefC q in
   let cbyte = cref (q_byte ()) in
diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli
index e81de603d9..1e25758572 100644
--- a/plugins/syntax/string_notation.mli
+++ b/plugins/syntax/string_notation.mli
@@ -13,6 +13,6 @@ open Vernacexpr
 
 (** * String notation *)
 
-val vernac_string_notation : Environ.env -> Evd.evar_map -> locality_flag ->
+val vernac_string_notation : locality_flag ->
                              qualid -> qualid -> qualid ->
                              Notation_term.scope_name -> unit