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/numeral.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/syntax/numeral.mli')

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