Stop using pstate in global print queries

Using pstate makes no sense for printing global stuff

5 files changed, 39 insertions, 49 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