diff options
| author | Lasse Blaauwbroek | 2020-09-06 22:21:18 +0200 |
|---|---|---|
| committer | Lasse Blaauwbroek | 2020-09-06 22:21:18 +0200 |
| commit | 5a417e9e25713e65bbe5f2a9c8fccef4d17bc4a6 (patch) | |
| tree | 3ca2a3ec3ff7340dfa91ff0e1d2871cd5d5178c0 | |
| parent | 48f465dd5c5f9db416a7cd57b0acb86f17323ce3 (diff) | |
Fix printing of `change` tactic, which was printed as `change_no_check` and vice versa
| -rw-r--r-- | plugins/ltac/pptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
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) ++ ( |