diff options
Diffstat (limited to 'parsing/pptactic.ml')
| -rw-r--r-- | parsing/pptactic.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index da915a5cc3..448b78e262 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -821,14 +821,15 @@ and pr_atom1 = function | TacTransitivity c -> str "transitivity" ++ pr_constrarg c (* Equality and inversion *) - | TacRewrite (ev,l,cl) -> + | TacRewrite (ev,l,cl,by) -> hov 1 (str (if ev then "erewrite" else "rewrite") ++ prlist_with_sep (fun () -> str ","++spc()) (fun (b,m,c) -> pr_orient b ++ spc() ++ pr_multi m ++ pr_with_bindings c) l - ++ pr_clauses pr_ident cl) + ++ pr_clauses pr_ident cl + ++ (match by with Some by -> pr_by_tactic (pr_tac_level ltop) by | None -> mt())) | TacInversion (DepInversion (k,c,ids),hyp) -> hov 1 (str "dependent " ++ pr_induction_kind k ++ spc () ++ pr_quantified_hypothesis hyp ++ |