Fix printing of change tactic, which was printed as `change_no_chec…

…k` and vice versa
coq · Sep 6, 2020 · 5a417e9 · 5a417e9
1 parent 48f465d
commit 5a417e9
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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)
             ++ (