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_string.mlg | 19 ++-----------------
 1 file changed, 2 insertions(+), 17 deletions(-)

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

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