diff options
| author | Hugo Herbelin | 2017-11-07 15:20:53 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-11-24 18:03:56 +0100 |
| commit | 1161ccf74578c3190d296dc37f39edecf28cf078 (patch) | |
| tree | 852666e60de305821eb94cdeadb1923f45b87fed | |
| 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).
| -rw-r--r-- | plugins/ltac/pptactic.ml | 6 | ||||
| -rw-r--r-- | test-suite/output/ltac.out | 2 |
2 files changed, 5 insertions, 3 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index d707512457..4b9e0fff40 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 ") ++ diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 7f3cdad6ce..eb9f571022 100644 --- a/test-suite/output/ltac.out +++ b/test-suite/output/ltac.out @@ -1,7 +1,7 @@ The command has indeed failed with message: Ltac variable y depends on pattern variable name z which is not bound in current context. Ltac f x y z := - symmetry in x, y; auto with z; auto; intros **; clearbody x; generalize + symmetry in x, y; auto with z; auto; intros; clearbody x; generalize dependent z The command has indeed failed with message: In nested Ltac calls to "g1" and "refine (uconstr)", last call failed. |