Merge PR #10237: Fix some incorrect uses of proof-local environment

Reviewed-by: gares
Reviewed-by: ppedrot

13 files changed, 55 insertions, 89 deletions

diff --git a/plugins/ltac/g_rewrite.mlg b/plugins/ltac/g_rewrite.mlg
index 12b12bc7b0..2fad1f6b6a 100644
--- a/plugins/ltac/g_rewrite.mlg
+++ b/plugins/ltac/g_rewrite.mlg
@@ -310,12 +310,6 @@ TACTIC EXTEND setoid_transitivity
 END
 
 VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY
-| ![ proof ] [ "Print" "Rewrite" "HintDb" preident(s) ] ->
-  { (* This command should not use the proof env, keeping previous
-       behavior as requested in review. *)
-    fun ~pstate ->
-      let sigma, env = Option.cata Pfedit.get_current_context
-          (let e = Global.env () in Evd.from_env e, e) pstate in
-    Feedback.msg_notice (Autorewrite.print_rewrite_hintdb env sigma s);
-    pstate }
+| [ "Print" "Rewrite" "HintDb" preident(s) ] ->
+  { Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) }
 END
diff --git a/plugins/setoid_ring/g_newring.mlg b/plugins/setoid_ring/g_newring.mlg
index 6be556b2ae..5dfead2d7e 100644
--- a/plugins/setoid_ring/g_newring.mlg
+++ b/plugins/setoid_ring/g_newring.mlg
@@ -13,8 +13,6 @@
 open Ltac_plugin
 open Pp
 open Util
-open Libnames
-open Printer
 open Newring_ast
 open Newring
 open Stdarg
@@ -85,21 +83,10 @@ END
 
 VERNAC COMMAND EXTEND AddSetoidRing CLASSIFIED AS SIDEFF
   | [ "Add" "Ring" ident(id) ":" constr(t) ring_mods_opt(l) ] ->
-    { let l = match l with None -> [] | Some l -> l in add_theory id t l }
-  | ![proof] [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> {
-    fun ~pstate ->
-    Feedback.msg_notice (strbrk "The following ring structures have been declared:");
-    Spmap.iter (fun fn fi ->
-      (* We should use the global env here as this shouldn't contain proof
-         data, however preserving behavior as requested in review. *)
-      let sigma, env = Option.cata Pfedit.get_current_context
-          (let e = Global.env () in Evd.from_env e, e) pstate in
-      Feedback.msg_notice (hov 2
-        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
-          str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++
-          str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req))
-    ) !from_name;
-    pstate }
+    { add_theory id t (Option.default [] l) }
+  | [ "Print" "Rings" ] => { Vernacextend.classify_as_query } -> {
+    print_rings ()
+  }
 END
 
 TACTIC EXTEND ring_lookup
@@ -135,20 +122,9 @@ END
 VERNAC COMMAND EXTEND AddSetoidField CLASSIFIED AS SIDEFF
 | [ "Add" "Field" ident(id) ":" constr(t) field_mods_opt(l) ] ->
   { let l = match l with None -> [] | Some l -> l in add_field_theory id t l }
-| ![proof] [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> {
-    fun ~pstate ->
-    Feedback.msg_notice (strbrk "The following field structures have been declared:");
-    Spmap.iter (fun fn fi ->
-      (* We should use the global env here as this shouldn't
-         contain proof data. *)
-      let sigma, env = Option.cata Pfedit.get_current_context
-          (let e = Global.env () in Evd.from_env e, e) pstate in
-      Feedback.msg_notice (hov 2
-        (Ppconstr.pr_id (Libnames.basename fn)++spc()++
-          str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
-          str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
-    ) !field_from_name;
-    pstate }
+| [ "Print" "Fields" ] => {Vernacextend.classify_as_query} -> {
+    print_fields ()
+  }
 END
 
 TACTIC EXTEND field_lookup
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b02b97f656..aeceeb4e50 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -327,6 +327,18 @@ module Cmap = Map.Make(Constr)
 let from_carrier = Summary.ref Cmap.empty ~name:"ring-tac-carrier-table"
 let from_name = Summary.ref Spmap.empty ~name:"ring-tac-name-table"
 
+let print_rings () =
+  Feedback.msg_notice (strbrk "The following ring structures have been declared:");
+  Spmap.iter (fun fn fi ->
+      let env = Global.env () in
+      let sigma = Evd.from_env env in
+      Feedback.msg_notice
+        (hov 2
+           (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+            str"with carrier "++ pr_constr_env env sigma fi.ring_carrier++spc()++
+            str"and equivalence relation "++ pr_constr_env env sigma fi.ring_req))
+    ) !from_name
+
 let ring_for_carrier r = Cmap.find r !from_carrier
 
 let find_ring_structure env sigma l =
@@ -824,6 +836,18 @@ let dest_field env evd th_spec =
 let field_from_carrier = Summary.ref Cmap.empty ~name:"field-tac-carrier-table"
 let field_from_name = Summary.ref Spmap.empty ~name:"field-tac-name-table"
 
+let print_fields () =
+  Feedback.msg_notice (strbrk "The following field structures have been declared:");
+  Spmap.iter (fun fn fi ->
+      let env = Global.env () in
+      let sigma = Evd.from_env env in
+      Feedback.msg_notice
+        (hov 2
+           (Ppconstr.pr_id (Libnames.basename fn)++spc()++
+            str"with carrier "++ pr_constr_env env sigma fi.field_carrier++spc()++
+            str"and equivalence relation "++ pr_constr_env env sigma fi.field_req))
+    ) !field_from_name
+
 let field_for_carrier r = Cmap.find r !field_from_carrier
 
 let find_field_structure env sigma l =
diff --git a/plugins/setoid_ring/newring.mli b/plugins/setoid_ring/newring.mli
index fcd04a2e73..3a21a82c5c 100644
--- a/plugins/setoid_ring/newring.mli
+++ b/plugins/setoid_ring/newring.mli
@@ -10,7 +10,6 @@
 
 open Names
 open EConstr
-open Libnames
 open Constrexpr
 open Newring_ast
 
@@ -23,7 +22,7 @@ val add_theory :
   constr_expr ->
   constr_expr ring_mod list -> unit
 
-val from_name : ring_info Spmap.t ref
+val print_rings : unit -> unit
 
 val ring_lookup :
   Geninterp.Val.t ->
@@ -35,7 +34,7 @@ val add_field_theory :
   constr_expr ->
   constr_expr field_mod list -> unit
 
-val field_from_name : field_info Spmap.t ref
+val print_fields : unit -> unit
 
 val field_lookup :
   Geninterp.Val.t ->
diff --git a/plugins/ssr/ssrvernac.mlg b/plugins/ssr/ssrvernac.mlg
index 08f028465b..8880a6516e 100644
--- a/plugins/ssr/ssrvernac.mlg
+++ b/plugins/ssr/ssrvernac.mlg
@@ -566,12 +566,10 @@ let print_view_hints env sigma kind l =
 }
 
 VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY
-| ![proof] [ "Print" "Hint" "View" ssrviewpos(i) ] ->
+| [ "Print" "Hint" "View" ssrviewpos(i) ] ->
   {
-    fun ~pstate ->
-    (* XXX this is incorrect *)
-    let sigma, env = Option.cata Pfedit.get_current_context
-        (let e = Global.env () in Evd.from_env e, e) pstate in
+    let env = Global.env () in
+    let sigma = Evd.from_env env in
     (match i with
     | Some k ->
       print_view_hints env sigma k (Ssrview.AdaptorDb.get k)
@@ -579,8 +577,7 @@ VERNAC COMMAND EXTEND PrintView CLASSIFIED AS QUERY
         List.iter (fun k -> print_view_hints env sigma k (Ssrview.AdaptorDb.get k))
           [ Ssrview.AdaptorDb.Forward;
             Ssrview.AdaptorDb.Backward;
-            Ssrview.AdaptorDb.Equivalence ]);
-    pstate
+            Ssrview.AdaptorDb.Equivalence ])
   }
 END
 
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
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
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml
index ec8c2338fb..b0b6fa69bb 100644
--- a/plugins/syntax/numeral.ml
+++ b/plugins/syntax/numeral.ml
@@ -101,7 +101,9 @@ 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 or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).")
 
-let vernac_numeral_notation env sigma local ty f g scope opts =
+let vernac_numeral_notation local ty f g scope opts =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
   let dec_ty = locate_decimal () in
   let z_pos_ty = locate_z () in
   let int63_ty = locate_int63 () in
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
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
diff --git a/plugins/syntax/string_notation.mli b/plugins/syntax/string_notation.mli
index e81de603d9..1e25758572 100644
--- a/plugins/syntax/string_notation.mli
+++ b/plugins/syntax/string_notation.mli
@@ -13,6 +13,6 @@ open Vernacexpr
 
 (** * String notation *)
 
-val vernac_string_notation : Environ.env -> Evd.evar_map -> locality_flag ->
+val vernac_string_notation : locality_flag ->
                              qualid -> qualid -> qualid ->
                              Notation_term.scope_name -> unit
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 51708670f5..4b1b473b33 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -75,7 +75,9 @@ let find_matches bas pat =
   let res = HintDN.search_pattern base pat in
   List.map snd res
 
-let print_rewrite_hintdb env sigma bas =
+let print_rewrite_hintdb bas =
+  let env = Global.env () in
+  let sigma = Evd.from_env env in
   (str "Database " ++ str bas ++ fnl () ++
 	   prlist_with_sep fnl
 	   (fun h ->
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index 03e9414e0f..4c6146d745 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -42,7 +42,7 @@ val auto_multi_rewrite : ?conds:conditions -> string list -> Locus.clause -> uni
 
 val auto_multi_rewrite_with : ?conds:conditions -> unit Proofview.tactic -> string list -> Locus.clause -> unit Proofview.tactic
 
-val print_rewrite_hintdb : Environ.env -> Evd.evar_map -> string -> Pp.t
+val print_rewrite_hintdb : string -> Pp.t
 
 open Clenv