From cb586ea65a1ad38626b7481ff8b30007f488705d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 9 Jun 2010 10:08:53 +0000
Subject: Backported r13080 (support for open terms in ltac matching) from
 trunk to v8.3. Also updated perf-analysis file (the part of the commit that
 delays typing of ltac instances seems to slightly improve a few
 contributions)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13096 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/ltac.v | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'test-suite')

diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index dfa41c820a..bbaeb08992 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.
-- 
cgit v1.2.3