From b913a79738fee897bc298e0804617da8abcb4cf5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 28 Apr 2019 16:29:16 +0200
Subject: Exposing a change_no_check tactic.

---
 plugins/ltac/pptactic.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac/pptactic.ml')

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 80070a7493..79f0f521cc 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -833,9 +833,10 @@ let pr_goal_selector ~toplevel s =
             pr_red_expr r
             ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
           )
-        | TacChange (op,c,h) ->
+        | TacChange (check,op,c,h) ->
+          let name = if check then "change_no_check" else "change" in
           hov 1 (
-            primitive "change" ++ brk (1,1)
+            primitive name ++ brk (1,1)
             ++ (
               match op with
                   None ->
-- 
cgit v1.2.3