From 5a417e9e25713e65bbe5f2a9c8fccef4d17bc4a6 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek
Date: Sun, 6 Sep 2020 22:21:18 +0200
Subject: Fix printing of `change` tactic, which was printed as
 `change_no_check` and vice versa

---
 plugins/ltac/pptactic.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 6233807016..f69fe064a7 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -831,7 +831,7 @@ let pr_goal_selector ~toplevel s =
             ++ pr_non_empty_arg (pr_clauses (Some true) pr.pr_name) h
           )
         | TacChange (check,op,c,h) ->
-          let name = if check then "change_no_check" else "change" in
+          let name = if check then "change" else "change_no_check" in
           hov 1 (
             primitive name ++ brk (1,1)
             ++ (
-- 
cgit v1.2.3