diff options
| author | Pierre-Marie Pédrot | 2020-09-08 10:36:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-08 10:36:42 +0200 |
| commit | edb2cefe61d5f5b3230ab33842e61423ca02fbdb (patch) | |
| tree | 51c6f669f233bee29f7371d97e353f4dab87472a | |
| parent | b972cc5195e941633319c1fa428a9801ac4ef9e2 (diff) | |
| parent | 5a417e9e25713e65bbe5f2a9c8fccef4d17bc4a6 (diff) | |
Merge PR #12987: Fix printing of `change` tactic
Reviewed-by: ppedrot
| -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) ++ ( |