Stop accessing proof env via Pfedit in printers

This should make https://github.com/coq/coq/pull/9129 easier.

6 files changed, 38 insertions, 34 deletions

diff --git a/plugins/syntax/g_numeral.mlg b/plugins/syntax/g_numeral.mlg
index 13e0bcbd47..73a2b99434 100644
--- a/plugins/syntax/g_numeral.mlg
+++ b/plugins/syntax/g_numeral.mlg
@@ -37,5 +37,6 @@ END
 VERNAC COMMAND EXTEND NumeralNotation CLASSIFIED AS SIDEFF
   | #[ locality = Attributes.locality; ] [ "Numeral" "Notation" reference(ty) reference(f) reference(g) ":"
       ident(sc) numnotoption(o) ] ->
-    { vernac_numeral_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) o }
+    { let (sigma, env) = Pfedit.get_current_context () in
+      vernac_numeral_notation env sigma (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 1e06cd8ddb..171e0e213d 100644
--- a/plugins/syntax/g_string.mlg
+++ b/plugins/syntax/g_string.mlg
@@ -21,5 +21,6 @@ open Stdarg
 VERNAC COMMAND EXTEND StringNotation CLASSIFIED AS SIDEFF
   | #[ locality = Attributes.locality; ] [ "String" "Notation" reference(ty) reference(f) reference(g) ":"
       ident(sc) ] ->
-    { vernac_string_notation (Locality.make_module_locality locality) ty f g (Id.to_string sc) }
+    { let (sigma, env) = Pfedit.get_current_context () in
+      vernac_string_notation env sigma (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 0c6d2ac0d1..525056e5f1 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -77,8 +77,7 @@ let locate_int63 () =
     Some (mkRefC q_int63)
   else None
 
-let has_type f ty =
-  let (sigma, env) = Pfedit.get_current_context () in
+let has_type env sigma f ty =
   let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
   try let _ = Constrintern.interp_constr env sigma c in true
   with Pretype_errors.PretypeError _ -> false
@@ -95,7 +94,7 @@ 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 could be used (you may need to require BinNums or Decimal or Int63 first).")
 
-let vernac_numeral_notation local ty f g scope opts =
+let vernac_numeral_notation env sigma local ty f g scope opts =
   let int_ty = locate_int () in
   let z_pos_ty = locate_z () in
   let int63_ty = locate_int63 () in
@@ -112,35 +111,35 @@ let vernac_numeral_notation local ty f g scope opts =
   (* Check the type of f *)
   let to_kind =
     match int_ty with
-    | Some (int_ty, cint, _) when has_type f (arrow cint cty) -> Int int_ty, Direct
-    | Some (int_ty, cint, _) when has_type f (arrow cint (opt cty)) -> Int int_ty, Option
-    | Some (int_ty, _, cuint) when has_type f (arrow cuint cty) -> UInt int_ty.uint, Direct
-    | Some (int_ty, _, cuint) when has_type f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option
+    | Some (int_ty, cint, _) when has_type env sigma f (arrow cint cty) -> Int int_ty, Direct
+    | Some (int_ty, cint, _) when has_type env sigma f (arrow cint (opt cty)) -> Int int_ty, Option
+    | Some (int_ty, _, cuint) when has_type env sigma f (arrow cuint cty) -> UInt int_ty.uint, Direct
+    | Some (int_ty, _, cuint) when has_type env sigma f (arrow cuint (opt cty)) -> UInt int_ty.uint, Option
     | _ ->
     match z_pos_ty with
-    | Some (z_pos_ty, cZ) when has_type f (arrow cZ cty) -> Z z_pos_ty, Direct
-    | Some (z_pos_ty, cZ) when has_type f (arrow cZ (opt cty)) -> Z z_pos_ty, Option
+    | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ cty) -> Z z_pos_ty, Direct
+    | Some (z_pos_ty, cZ) when has_type env sigma f (arrow cZ (opt cty)) -> Z z_pos_ty, Option
     | _ ->
     match int63_ty with
-    | Some cint63 when has_type f (arrow cint63 cty) -> Int63, Direct
-    | Some cint63 when has_type f (arrow cint63 (opt cty)) -> Int63, Option
+    | Some cint63 when has_type env sigma f (arrow cint63 cty) -> Int63, Direct
+    | Some cint63 when has_type env sigma f (arrow cint63 (opt cty)) -> Int63, Option
     | _ -> type_error_to f ty
   in
   (* Check the type of g *)
   let of_kind =
     match int_ty with
-    | Some (int_ty, cint, _) when has_type g (arrow cty cint) -> Int int_ty, Direct
-    | Some (int_ty, cint, _) when has_type g (arrow cty (opt cint)) -> Int int_ty, Option
-    | Some (int_ty, _, cuint) when has_type g (arrow cty cuint) -> UInt int_ty.uint, Direct
-    | Some (int_ty, _, cuint) when has_type g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option
+    | Some (int_ty, cint, _) when has_type env sigma g (arrow cty cint) -> Int int_ty, Direct
+    | Some (int_ty, cint, _) when has_type env sigma g (arrow cty (opt cint)) -> Int int_ty, Option
+    | Some (int_ty, _, cuint) when has_type env sigma g (arrow cty cuint) -> UInt int_ty.uint, Direct
+    | Some (int_ty, _, cuint) when has_type env sigma g (arrow cty (opt cuint)) -> UInt int_ty.uint, Option
     | _ ->
     match z_pos_ty with
-    | Some (z_pos_ty, cZ) when has_type g (arrow cty cZ) -> Z z_pos_ty, Direct
-    | Some (z_pos_ty, cZ) when has_type g (arrow cty (opt cZ)) -> Z z_pos_ty, Option
+    | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty cZ) -> Z z_pos_ty, Direct
+    | Some (z_pos_ty, cZ) when has_type env sigma g (arrow cty (opt cZ)) -> Z z_pos_ty, Option
     | _ ->
     match int63_ty with
-    | Some cint63 when has_type g (arrow cty cint63) -> Int63, Direct
-    | Some cint63 when has_type g (arrow cty (opt cint63)) -> Int63, Option
+    | Some cint63 when has_type env sigma g (arrow cty cint63) -> Int63, Direct
+    | Some cint63 when has_type env sigma g (arrow cty (opt cint63)) -> Int63, Option
     | _ -> type_error_of g ty
   in
   let o = { to_kind; to_ty; of_kind; of_ty;
diff --git a/plugins/syntax/numeral.mli b/plugins/syntax/numeral.mli
index f96b8321f8..b14ed18497 100644
--- a/plugins/syntax/numeral.mli
+++ b/plugins/syntax/numeral.mli
@@ -14,4 +14,6 @@ open Notation
 
 (** * Numeral notation *)
 
-val vernac_numeral_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> numnot_option -> unit
+val vernac_numeral_notation : Environ.env -> Evd.evar_map -> 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 12ee4c6eda..5fae696d58 100644
--- a/plugins/syntax/string_notation.ml
+++ b/plugins/syntax/string_notation.ml
@@ -32,8 +32,7 @@ let q_option () = qualid_of_ref "core.option.type"
 let q_list () = qualid_of_ref "core.list.type"
 let q_byte () = qualid_of_ref "core.byte.type"
 
-let has_type f ty =
-  let (sigma, env) = Pfedit.get_current_context () in
+let has_type env sigma f ty =
   let c = mkCastC (mkRefC f, Glob_term.CastConv ty) in
   try let _ = Constrintern.interp_constr env sigma c in true
   with Pretype_errors.PretypeError _ -> false
@@ -48,7 +47,7 @@ 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 local ty f g scope =
+let vernac_string_notation env sigma local ty f g scope =
   let app x y = mkAppC (x,[y]) in
   let cref q = mkRefC q in
   let cbyte = cref (q_byte ()) in
@@ -66,18 +65,18 @@ let vernac_string_notation local ty f g scope =
   let constructors = get_constructors tyc in
   (* Check the type of f *)
   let to_kind =
-    if has_type f (arrow clist_byte cty) then ListByte, Direct
-    else if has_type f (arrow clist_byte (opt cty)) then ListByte, Option
-    else if has_type f (arrow cbyte cty) then Byte, Direct
-    else if has_type f (arrow cbyte (opt cty)) then Byte, Option
+    if has_type env sigma f (arrow clist_byte cty) then ListByte, Direct
+    else if has_type env sigma f (arrow clist_byte (opt cty)) then ListByte, Option
+    else if has_type env sigma f (arrow cbyte cty) then Byte, Direct
+    else if has_type env sigma f (arrow cbyte (opt cty)) then Byte, Option
     else type_error_to f ty
   in
   (* Check the type of g *)
   let of_kind =
-    if has_type g (arrow cty clist_byte) then ListByte, Direct
-    else if has_type g (arrow cty (opt clist_byte)) then ListByte, Option
-    else if has_type g (arrow cty cbyte) then Byte, Direct
-    else if has_type g (arrow cty (opt cbyte)) then Byte, Option
+    if has_type env sigma g (arrow cty clist_byte) then ListByte, Direct
+    else if has_type env sigma g (arrow cty (opt clist_byte)) then ListByte, Option
+    else if has_type env sigma g (arrow cty cbyte) then Byte, Direct
+    else if has_type env sigma g (arrow cty (opt cbyte)) then Byte, Option
     else type_error_of g ty
   in
   let o = { to_kind = to_kind;
diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli
index 9a0174abf2..e81de603d9 100644
--- a/plugins/syntax/string_notation.mli
+++ b/plugins/syntax/string_notation.mli
@@ -13,4 +13,6 @@ open Vernacexpr
 
 (** * String notation *)
 
-val vernac_string_notation : locality_flag -> qualid -> qualid -> qualid -> Notation_term.scope_name -> unit
+val vernac_string_notation : Environ.env -> Evd.evar_map -> locality_flag ->
+                             qualid -> qualid -> qualid ->
+                             Notation_term.scope_name -> unit