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

Reviewed-by: gares
Reviewed-by: ppedrot

3 files changed, 33 insertions, 34 deletions

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 ->