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/string_notation.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'plugins/syntax/string_notation.ml')

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