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
---
 CHANGES                   |  2 ++
 dev/doc/perf-analysis     |  8 ++++++--
 test-suite/success/ltac.v | 23 +++++++++++++++++++++++
 3 files changed, 31 insertions(+), 2 deletions(-)

diff --git a/CHANGES b/CHANGES
index e41dbdd062..a4cd4118ab 100644
--- a/CHANGES
+++ b/CHANGES
@@ -75,6 +75,8 @@ Other tactics
 - In "simpl c" and "change c with d", c can be a pattern.
 - Tactic "revert" now preserves let-in's making it the exact inverse of
   "intro".
+- Ltac's pattern-matching now supports matching metavariables that
+  depend on variables bound upwards in the pattern.
 
 Tactic definitions
 
diff --git a/dev/doc/perf-analysis b/dev/doc/perf-analysis
index 805f0778d1..ac54fa6f73 100644
--- a/dev/doc/perf-analysis
+++ b/dev/doc/perf-analysis
@@ -1,9 +1,13 @@
 Performance analysis (trunk repository)
 ---------------------------------------
 
-Jun 4, 2010: improvement in type classes inference by removing
+Jun 7, 2010: delayed re-typing of Ltac instances in matching
+  (-1% on HighSchoolGeometry, -2% on JordanCurveTheorem)
+
+Jun 4, 2010: improvement in eauto and type classes inference by removing
   systematic preparation of debugging pretty-printing streams (std_ppcmds)
-  (-7% in ATBR, visible only on V8.3 logs since ATBR is broken in trunk)
+  (-7% in ATBR, visible only on V8.3 logs since ATBR is broken in trunk;
+   -6% in HighSchoolGeometry)
 
 Apr 19, 2010: small improvement obtained by reducing evar instantiation 
   from O(n^3) to O(n^2) in the size of the instance (-2% in Compcert,
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