2 files changed, 37 insertions, 0 deletions
diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 20e274e254..21a8cf9ede 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -3,3 +3,22 @@ Error: Ltac variable y depends on pattern variable name z which is not bound in
 Ltac f x y z :=
   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", last call failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+In nested Ltac calls to "f1" and "refine", last call failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+In nested Ltac calls to "g2", "g1" and "refine", last call failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+In nested Ltac calls to "f2", "f1" and "refine", last call failed.
+The term "I" has type "True" while it is expected to have type "False".
+The command has indeed failed with message:
+Ltac call to "h" failed.
+Error: Ltac variable x is bound to I which cannot be coerced to
+a declared or quantified hypothesis.
+The command has indeed failed with message:
+In nested Ltac calls to "h" and "injection", last call failed.
+Error: No primitive equality found.
diff --git a/test-suite/output/ltac.v b/test-suite/output/ltac.v
index 373b870b9f..dfa60eeda0 100644
--- a/test-suite/output/ltac.v
+++ b/test-suite/output/ltac.v
@@ -25,3 +25,21 @@ Ltac f x y z :=
   generalize dependent z.
 
 Print Ltac f.
+
+(* Error messages *)
+
+Ltac g1 x := refine x.
+Tactic Notation "g2" constr(x) := g1 x.
+Tactic Notation "f1" constr(x) := refine x.
+Ltac f2 x := f1 x.
+Goal False.
+Fail g1 I.
+Fail f1 I.
+Fail g2 I.
+Fail f2 I.
+
+Ltac h x := injection x.
+Goal True -> False.
+Fail h I.
+intro H.
+Fail h H.