aboutsummaryrefslogtreecommitdiffhomepage
path: root/test-suite
diff options
context:
space:
mode:
Diffstat (limited to 'test-suite')
-rw-r--r--test-suite/success/ltac.v23
1 files changed, 23 insertions, 0 deletions
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index dfa41c820..bbaeb0899 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -243,3 +243,26 @@ test_open_match (forall z y, y + z = 0).
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.