Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 10 insertions, 4 deletions

diff --git a/test-suite/output/ltac.out b/test-suite/output/ltac.out
index 1ff09e3a..eb9f5710 100644
--- a/test-suite/output/ltac.out
+++ b/test-suite/output/ltac.out
@@ -1,8 +1,7 @@
 The command has indeed failed with message:
-Error:
 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.
@@ -22,13 +21,20 @@ 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 "h" and "injection (destruction_arg)", last call
 failed.
-Error: No primitive equality found.
+No primitive equality found.
 The command has indeed failed with message:
 In nested Ltac calls to "h" and "injection (destruction_arg)", last call
 failed.
-Error: No primitive equality found.
+No primitive equality found.
 Hx
 nat
 nat
 0
 0
+Ltac foo :=
+  let x := intros in
+  let y := intros -> in
+  let v := constr:(nil) in
+  let w := () in
+  let z := 1 in
+  pose v