From 1161ccf74578c3190d296dc37f39edecf28cf078 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 7 Nov 2017 15:20:53 +0100 Subject: Printing again "intros **" as "intros" by default. The rationale it that it is more common to do so and thus more "natural" (principle of writing less whenever possible). --- plugins/ltac/pptactic.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) (limited to 'plugins/ltac/pptactic.ml') diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d70751245..4b9e0fff4 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -723,8 +723,10 @@ let pr_goal_selector ~toplevel s = | TacIntroPattern (ev,[]) as t -> pr_atom0 t | 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) + hov 1 (primitive (if ev then "eintros" else "intros") ++ + (match p with + | [_,Misctypes.IntroForthcoming false] -> mt () + | _ -> spc () ++ prlist_with_sep spc (Miscprint.pr_intro_pattern pr.pr_dconstr) p)) | TacApply (a,ev,cb,inhyp) -> hov 1 ( (if a then mt() else primitive "simple ") ++ -- cgit v1.2.3