From 46056cbe56f9c39fe3f8f5175aff9fd6427684b6 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Sun, 5 May 2019 17:11:06 +0200
Subject: Stop using pstate in global print queries

Using pstate makes no sense for printing global stuff
---
 plugins/ltac/g_rewrite.mlg | 10 ++--------
 1 file changed, 2 insertions(+), 8 deletions(-)

(limited to 'plugins/ltac')

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
-- 
cgit v1.2.3