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

Reviewed-by: gares
Reviewed-by: ppedrot

1 files changed, 2 insertions, 8 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