diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f8b34e249..bc39c9304 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -845,17 +845,18 @@ module Make (* Printing tactics as arguments *) let rec pr_atom0 a = tag_atom a (match a with - | TacIntroPattern [] -> primitive "intros" + | TacIntroPattern (false,[]) -> primitive "intros" + | TacIntroPattern (true,[]) -> primitive "eintros" | t -> str "(" ++ pr_atom1 t ++ str ")" ) (* Main tactic printer *) and pr_atom1 a = tag_atom a (match a with (* Basic tactics *) - | TacIntroPattern [] as t -> + | TacIntroPattern (ev,[]) as t -> pr_atom0 t - | TacIntroPattern (_::_ as p) -> - hov 1 (primitive "intros" ++ spc () ++ + | TacIntroPattern (ev,(_::_ as p)) -> + hov 1 (primitive (if ev then "eintros" else "intros") ++ spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p) | TacApply (a,ev,cb,inhyp) -> hov 1 ( |