diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-07 15:20:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-11-24 18:03:56 +0100 |
| commit | 1161ccf74578c3190d296dc37f39edecf28cf078 (patch) | |
| tree | 852666e60de305821eb94cdeadb1923f45b87fed /plugins/ltac/pptactic.ml | |
| parent | e59d58b6db222332f7d7ad2adcb2b78c24fb351e (diff) | |
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).
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 6 |
1 files changed, 4 insertions, 2 deletions
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 ") ++ |