From 824b2393c9cc180c82dba00ee710124c24184945 Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 24 May 2019 16:35:09 +0200
Subject: Use global env in numeral and string notations

Since their introduction, these notations were incorrectly using the
proof-local environment.
---
 plugins/syntax/g_numeral.mlg | 19 ++-----------------
 1 file changed, 2 insertions(+), 17 deletions(-)

(limited to 'plugins/syntax/g_numeral.mlg')

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
-- 
cgit v1.2.3