Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 27 insertions, 0 deletions

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 02618c2c..7387add6 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -244,6 +244,29 @@ reflexivity.
 apply I.
 Qed.
 
+(* Test binding of open terms with non linear matching *)
+
+Ltac f_non_linear t :=
+  match t with
+    (forall x y, ?u = 0) -> (forall y x, ?u = 0) =>
+       assert (forall x y:nat, u = u)
+  end.
+
+Goal True.
+f_non_linear ((forall x y, x+y = 0) -> (forall x y, y+x = 0)).
+reflexivity.
+f_non_linear ((forall a b, a+b = 0) -> (forall a b, b+a = 0)).
+reflexivity.
+f_non_linear ((forall a b, a+b = 0) -> (forall x y, y+x = 0)).
+reflexivity.
+f_non_linear ((forall x y, x+y = 0) -> (forall a b, b+a = 0)).
+reflexivity.
+f_non_linear ((forall x y, x+y = 0) -> (forall y x, x+y = 0)).
+reflexivity.
+f_non_linear ((forall x y, x+y = 0) -> (forall y x, y+x = 0)) (* should fail *)
+|| exact I.
+Qed.
+
 (* Test regular failure when clear/intro breaks soundness of the
    interpretation of terms in current environment *)
 
@@ -275,3 +298,7 @@ evar(foo:nat).
 let evval := eval compute in foo in not_eq evval 1.
 let evval := eval compute in foo in not_eq 1 evval.
 Abort.
+
+(* Check that this returns an error and not an anomaly (see r13667) *)
+
+Fail Local Tactic Notation "myintro" := intro.