diff options
| -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 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 ") ++ diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out index 7f3cdad6c..eb9f57102 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. |