diff options
| author | Gaëtan Gilbert | 2019-05-05 17:11:06 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-05-24 16:23:32 +0200 |
| commit | 46056cbe56f9c39fe3f8f5175aff9fd6427684b6 (patch) | |
| tree | 9c70ee243a2f5025bea4f7c8306d7cbd25f5d66f /plugins/ltac | |
| parent | 831639deec0ce88fca4ede4756815cf434088ac3 (diff) | |
Stop using pstate in global print queries
Using pstate makes no sense for printing global stuff
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/g_rewrite.mlg | 10 |
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 |