From v8.2 to trunk:

- commit 11871 (Miller's pattern detection bug) + a corresponding test
- commit 11883 (.ml4 to .cmxs in coq_makefile) 



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11884 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 9 insertions, 0 deletions

diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 082cbfbe1..e3a6e4188 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -198,6 +198,15 @@ Goal forall x : nat, F1 x -> G1 x.
 refine (fun x H => proj2 (_ x H) _).
 Abort.
 
+
+(* An example from y-not that was failing in 8.2rc1 *)
+
+Fixpoint filter (A:nat->Set) (l:list (sigT A)) : list (sigT A) := 
+  match l with
+  | nil => nil
+  | (existT k v)::l' => (existT _ k v):: (filter A l')
+  end.
+
 (* Remark: the following example does not succeed any longer in 8.2 because,
    the algorithm is more general and does exclude a solution that it should
    exclude for typing reason. Handling of types and backtracking is still to