Imported Upstream version 8.4~betaupstream/8.4_beta

50 files changed, 1493 insertions, 293 deletions

diff --git a/test-suite/success/AdvancedCanonicalStructure.v b/test-suite/success/AdvancedCanonicalStructure.v
index b533db6e..97cf316c 100644
--- a/test-suite/success/AdvancedCanonicalStructure.v
+++ b/test-suite/success/AdvancedCanonicalStructure.v
@@ -79,19 +79,17 @@ Record interp_pair :Type :=
     link: abs = interp repr }.
 
 Lemma prod_interp :forall (a b:interp_pair),a * b = interp (Prod a b) .
-proof.
-let a:interp_pair,b:interp_pair.
-reconsider thesis as (a * b = interp a * interp b).
-thus thesis by (link a),(link b).
-end proof.
+Proof.
+intros a b.
+change (a * b = interp a * interp b).
+rewrite (link a), (link b); reflexivity.
 Qed.
 
 Lemma fun_interp :forall (a b:interp_pair), (a -> b) = interp (Fun a b).
-proof.
-let a:interp_pair,b:interp_pair.
-reconsider thesis as ((a -> b) = (interp a -> interp b)).
-thus thesis using rewrite (link a);rewrite (link b);reflexivity.
-end proof.
+Proof.
+intros a b.
+change ((a -> b) = (interp a -> interp b)).
+rewrite (link a), (link b); reflexivity.
 Qed.
 
 Canonical Structure ProdCan (a b:interp_pair) :=
diff --git a/test-suite/success/CaseAlias.v b/test-suite/success/CaseAlias.v
index 32d85779..a9249086 100644
--- a/test-suite/success/CaseAlias.v
+++ b/test-suite/success/CaseAlias.v
@@ -1,3 +1,4 @@
+(*********************************************)
 (* This has been a bug reported by Y. Bertot *)
 Inductive expr : Set :=
   | b : expr -> expr -> expr
@@ -19,3 +20,72 @@ Fixpoint f2 (t : expr) : expr :=
   | x => b x a
   end.
 
+(*********************************************)
+(* Test expansion of aliases                 *)
+(* Originally taken from NMake_gen.v         *)
+
+ Local Notation SizePlus n := (S (S (S (S (S (S n)))))).
+ Local Notation Size := (SizePlus O).
+
+ Parameter zn2z : Type -> Type.
+ Parameter w0 : Type.
+ Fixpoint word (w : Type) (n : nat) {struct n} : Type :=
+  match n with
+  | 0 => w
+  | S n0 => zn2z (word w n0)
+  end.
+
+ Definition w1 := zn2z w0.
+ Definition w2 := zn2z w1.
+ Definition w3 := zn2z w2.
+ Definition w4 := zn2z w3.
+ Definition w5 := zn2z w4.
+ Definition w6 := zn2z w5.
+
+ Definition dom_t n := match n with
+  | 0 => w0
+  | 1 => w1
+  | 2 => w2
+  | 3 => w3
+  | 4 => w4
+  | 5 => w5
+  | 6 => w6
+  | SizePlus n => word w6 n
+ end.
+Parameter plus_t : forall n m : nat, word (dom_t n) m -> dom_t (m + n).
+
+(* This used to fail because of a bug in expansion of SizePlus wrongly
+   reusing n as an alias for the subpattern *)
+Definition plus_t1 n : forall m, word (dom_t n) m -> dom_t (m+n) :=
+   match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with
+     | SizePlus (S n') as n => plus_t n
+     | _ as n =>
+         fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with
+                    | SizePlus (S (S m')) as m => plus_t n m
+                    | _ => fun x => x
+                  end
+   end.
+
+(* Test (useless) intermediate alias *)
+Definition plus_t2 n : forall m, word (dom_t n) m -> dom_t (m+n) :=
+   match n return (forall m, word (dom_t n) m -> dom_t (m+n)) with
+     | S (S (S (S (S (S (S n'))))) as n) as n'' => plus_t n''
+     | _ as n =>
+         fun m => match m return (word (dom_t n) m -> dom_t (m+n)) with
+                    | SizePlus (S (S m')) as m => plus_t n m
+                    | _ => fun x => x
+                  end
+   end.
+
+(*****************************************************************************)
+(* Check that alias expansion behaves consistently from versions to versions *)
+
+Definition g m :=
+  match pred m with
+  | 0 => 0
+  | n => n (* For compatibility, right-hand side should be (S n), not (pred m) *)
+  end.
+
+Goal forall m, g m = match pred m with 0 => 0 | S n => S n end.
+intro; reflexivity.
+Abort.
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index e63972ce..745529bf 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -543,7 +543,7 @@ Type
    end).
 
 (* Nested Cases: the SYNTH of the Cases on n used to make Multcase believe
- * it has to synthtize the predicate on O (which he can't)
+ * it has to synthesize the predicate on O (which he can't)
  *)
 Type
   match 0 as n return match n with
@@ -611,31 +611,52 @@ Type
    | Consn n a (Consn m b l) => n + m
    end).
 
-(*
-Type [A:Set][n:nat][l:(Listn A n)]
-                   <[_:nat](Listn A O)>Cases l of
-                         (Niln  as b) => b
-                      | (Consn  n a (Niln  as b))=> (Niln A)
-                      | (Consn  n a (Consn m b l)) => (Niln A)
-                      end.
-
-Type [A:Set][n:nat][l:(Listn A n)]
-                    Cases l of
-                         (Niln  as b) => b
-                      | (Consn  n a (Niln  as b))=> (Niln A)
-                      | (Consn  n a (Consn m b l)) => (Niln A)
-                      end.
+(* This example was deactivated in Cristina's code
+
+Type
+  (fun (A:Set) (n:nat) (l:Listn A n) =>
+    match l return Listn A O with
+      | Niln  as b => b
+      | Consn  n a (Niln  as b) => (Niln A)
+      | Consn  n a (Consn m b l) => (Niln A)
+    end).
+*)
+
+(* This one is (still) failing: too weak unification
+
+Type
+  (fun (A:Set) (n:nat) (l:Listn A n) =>
+    match l with
+      | Niln  as b => b
+      | Consn  n a (Niln  as b) => (Niln A)
+      | Consn  n a (Consn m b l) => (Niln A)
+    end).
+*)
+
+(* This one is failing: alias L not chosen of the right type
+
+Type
+  (fun (A:Set) (n:nat) (l:Listn A n) =>
+    match l return Listn A (S 0) with
+      | Niln  as b => Consn A O O b
+      | Consn n a Niln as L => L
+      | Consn n a _ => Consn A O O (Niln A)
+    end).
 *)
-(******** This example rises an error unconstrained_variables!
-Type [A:Set][n:nat][l:(Listn A n)]
-                    Cases l of
-                         (Niln  as b) => (Consn A O O b)
-                      | ((Consn  n a Niln) as L) =>  L
-                      | (Consn  n a _)  =>  (Consn A O O (Niln A))
-                      end.
+
+(******** This example (still) failed
+
+Type
+  (fun (A:Set) (n:nat) (l:Listn A n) =>
+    match l return Listn A (S 0) with
+      | Niln  as b => Consn A O O b
+      | Consn n a Niln as L => L
+      | Consn n a _ => Consn A O O (Niln A)
+    end).
+
 **********)
 
-(* To test tratement of as-patterns in depth *)
+(* To test treatment of as-patterns in depth *)
 Type
   (fun (A : Set) (l : List A) =>
    match l with
@@ -1064,7 +1085,7 @@ Type
    | Consn n a (Consn m b l) => fun _ : nat => n + m
    end).
 
-(* Alsos tests for multiple _ patterns *)
+(* Also tests for multiple _ patterns *)
 Type
   (fun (A : Set) (n : nat) (l : Listn A n) =>
    match l in (Listn _ n) return (Listn A n) with
@@ -1072,14 +1093,14 @@ Type
    | Consn _ _ _ as b => b
    end).
 
-(** Horrible error message!
+(** This one was said to raised once an "Horrible error message!" *)
 
-Type [A:Set][n:nat][l:(Listn A n)]
-                        Cases l of
-                        (Niln as b) => b
-                      | ((Consn _ _ _ ) as b)=>  b
-                      end.
-******)
+Type
+  (fun (A:Set) (n:nat) (l:Listn A n) =>
+   match l with
+   | Niln as b => b
+   | Consn _ _ _  as b =>  b
+   end).
 
 Type
   match niln in (listn n) return (listn n) with
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index 29721843..d3b7cf3f 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -26,6 +26,40 @@ Fixpoint foldrn (n : nat) (bs : listn B n) {struct bs} : C :=
   end.
 End Folding.
 
+(** Testing post-processing of nested dependencies *)
+
+Check fun x:{x|x=0}*nat+nat => match x with
+      | inl ((exist 0 eq_refl),0) => None
+      | _ => Some 0
+      end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x with
+      | inl (exist (exist 0 eq_refl) I) => None
+      | _ => Some 0
+      end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x with
+      | inl (exist (exist 0 eq_refl) I) => None
+      | _ => Some 0
+      end.
+
+Check fun x:{_:{x|x=0}|True}+nat => match x return option nat with
+      | inl (exist (exist 0 eq_refl) I) => None
+      | _ => Some 0
+      end.
+
+  (* the next two examples were failing from r14703 (Nov 22 2011) to r14732 *)
+  (* due to a bug in dependencies postprocessing (revealed by CoLoR) *)
+
+Check fun x:{x:nat*nat|fst x = 0 & True} => match x return option nat with
+      | exist2 (x,y) eq_refl I => None
+      end.
+
+Check fun x:{_:{x:nat*nat|fst x = 0 & True}|True}+nat => match x return option nat with
+      | inl (exist (exist2 (x,y) eq_refl I) I) => None
+      | _ => Some 0
+      end.
+
 (* -------------------------------------------------------------------- *)
 (*   Example to test patterns matching on dependent families            *)
 (* This exemple extracted from the developement done by Nacira Chabane  *)
@@ -506,3 +540,23 @@ Definition test (s:step E E) :=
     | Step nil _ (cons E nil) _ Plus l l' => true
     | _ => false
   end.
+
+(* Testing regression of bug 2454 ("get" used not be type-checkable when
+   defined with its type constraint) *)
+
+Inductive K : nat -> Type := KC : forall (p q:nat), K p.
+
+Definition get : K O -> nat := fun x => match x with KC p q => q end.
+
+(* Checking correct order of substitution of realargs *)
+(* (was broken from revision 14664 to 14669) *)
+(* Example extracted from contrib CoLoR *)
+
+Inductive EQ : nat -> nat -> Prop := R x y : EQ x y.
+
+Check fun e t (d1 d2:EQ e t) =>
+      match d1 in EQ e1 t1, d2 in EQ e2 t2 return
+        (e1,t1) = (e2,t2) -> (e1,t1) = (e,t) -> 0=0
+      with
+      | R _ _, R _ _ => fun _ _ => eq_refl
+      end.
diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v
index d5b94ab4..47180ef6 100644
--- a/test-suite/success/Check.v
+++ b/test-suite/success/Check.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/Discriminate.v b/test-suite/success/Discriminate.v
index dffad323..a7596741 100644
--- a/test-suite/success/Discriminate.v
+++ b/test-suite/success/Discriminate.v
@@ -32,3 +32,9 @@ intros.
 ediscriminate (H O).
 instantiate (1:=O).
 Abort.
+
+(* Check discriminate on identity *)
+
+Goal ~ identity 0 1.
+discriminate.
+Qed.
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v
index 08e8aed2..0efd90a1 100644
--- a/test-suite/success/Field.v
+++ b/test-suite/success/Field.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Field.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (**** Tests of Field with real numbers ****)
 
 Require Import Reals RealField.
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 4aa00e68..a93f8900 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -24,7 +24,7 @@ Hint Destruct h8 := 4 Hypothesis (_ <= _) => fun H => apply H.
 (* Checks that local names are accepted *)
 Section A.
   Remark Refl : forall (A : Set) (x : A), x = x.
-  Proof. exact refl_equal. Defined.
+  Proof. exact @refl_equal. Defined.
   Definition Sym := sym_equal.
   Let Trans := trans_equal.
 
diff --git a/test-suite/success/Inductive.v b/test-suite/success/Inductive.v
index 203fbbb7..da5dd5e4 100644
--- a/test-suite/success/Inductive.v
+++ b/test-suite/success/Inductive.v
@@ -54,6 +54,15 @@ Check
    | Build_B x0 x1 => f x0 x1
    end).
 
+(* Check inductive types with local definitions (constructors) *)
+
+Inductive I1 : Set := C1 (_:I1) (_:=0).
+
+Check (fun x:I1 =>
+  match x with
+  | C1 i n => (i,n)
+  end).
+
 (* Check implicit parameters of inductive types (submitted by Pierre
   Casteran and also implicit in #338) *)
 
@@ -78,3 +87,23 @@ Record P:Type := {PA:Set; PB:Set}.
 Definition F (p:P) := (PA p) -> (PB p).
 
 Inductive I_F:Set := c : (F (Build_P nat I_F)) -> I_F.
+
+(* Check that test for binders capturing implicit arguments is not stronger
+   than needed (problem raised by Cedric Auger) *)
+
+Set Implicit Arguments.
+Inductive bool_comp2 (b: bool): bool -> Prop :=
+| Opp2: forall q, (match b return Prop with
+                  | true => match q return Prop with 
+                              true => False |
+                              false => True end
+                  | false => match q return Prop with
+                              true => True |
+                              false => False end end) -> bool_comp2 b q.
+
+(* This one is still to be made acceptable...
+
+Set Implicit Arguments.
+Inductive I A : A->Prop := C a : (forall A, A) -> I a.
+
+ *)
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index 5091b44c..b068f729 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -73,15 +73,15 @@ Require Import Bvector.
 
 Inductive I : nat -> Set :=
   | C1 : I 1
-  | C2 : forall k i : nat, vector (I i) k -> I i.
+  | C2 : forall k i : nat, Vector.t (I i) k -> I i.
 
-Inductive SI : forall k : nat, I k -> vector nat k -> nat -> Prop :=
+Inductive SI : forall k : nat, I k -> Vector.t nat k -> nat -> Prop :=
     SC2 :
-      forall (k i vf : nat) (v : vector (I i) k) (xi : vector nat i),
+      forall (k i vf : nat) (v : Vector.t (I i) k) (xi : Vector.t nat i),
       SI (C2 v) xi vf.
 
 Theorem SUnique :
- forall (k : nat) (f : I k) (c : vector nat k) v v',
+ forall (k : nat) (f : I k) (c : Vector.t nat k) v v',
  SI f c v -> SI f c v' -> v = v'.
 Proof.
 induction 1.
@@ -129,3 +129,10 @@ Proof.
    an inconsistent state that disturbed "inversion" *)
 intros. inversion H.
 Abort.
+
+(* Bug #2314 (simplified): check that errors do not show as anomalies *)
+
+Goal True -> True.
+intro.
+Fail inversion H using False.
+Fail inversion foo using True_ind.
diff --git a/test-suite/success/LegacyField.v b/test-suite/success/LegacyField.v
index 53bcc63a..df4da431 100644
--- a/test-suite/success/LegacyField.v
+++ b/test-suite/success/LegacyField.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Field.v 7693 2005-12-21 23:50:17Z herbelin $ *)
-
 (**** Tests of Field with real numbers ****)
 
 Require Import Reals LegacyRfield.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 661a8757..f5f5a9d1 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -59,3 +59,30 @@ Check (fun x:nat*nat => match x with R x y => (x,y) end).
 Local Notation "[ a  # ; ..  # ; b ]" := (a + .. (b + 0) ..).   
 Check [ 0 ].
 Check [ 0 # ; 1 ].
+
+(* Check well-scoping of alpha-renaming of private binders *)
+(* see bug #2248 (thanks to Marc Lasson) *)
+
+Notation "{ q , r | P }" := (fun (p:nat*nat) => let (q, r) := p in P).
+Check (fun p => {q,r| q + r = p}).
+
+(* Check that declarations of empty levels are correctly backtracked *)
+
+Section B.
+Notation "*" := 5 (at level 0) : nat_scope.
+Notation "[ h ] p" := (h + p) (at level 8, p at level 9, h at level 7) : nat_scope.
+End B.
+
+(* Should succeed *)
+Definition n := 5 * 5.
+
+(* Check that lonely notations (here FOO) do not modify the visibility
+   of scoped interpretations (bug #2634 fixed in r14819) *)
+
+Notation "x ++++ y" := (mult x y) (at level 40).
+Notation "x ++++ y" := (plus x y) : A_scope.
+Open Scope A_scope.
+Notation "'FOO' x" := (S x) (at level 40).
+Goal (2 ++++ 3) = 5.
+reflexivity.
+Abort.
diff --git a/test-suite/success/Nsatz.v b/test-suite/success/Nsatz.v
index 518d22e9..d316e4a0 100644
--- a/test-suite/success/Nsatz.v
+++ b/test-suite/success/Nsatz.v
@@ -1,51 +1,27 @@
-Require Import Nsatz ZArith Reals List Ring_polynom.
+(* compile en user    3m39.915s sur cachalot *)
+Require Import Nsatz.
 
 (* Example with a generic domain *)
 
-Variable A: Type.
-Variable Ad: Domain A.
+Section test.
 
-Definition Ari : Ring A:= (@domain_ring A Ad).
-Existing Instance Ari.
-
-Existing Instance ring_setoid.
-Existing Instance ring_plus_comp.
-Existing Instance ring_mult_comp.
-Existing Instance ring_sub_comp.
-Existing Instance ring_opp_comp.
-
-Add Ring Ar: (@ring_ring A (@domain_ring A Ad)).
-
-Instance zero_ring2 : Zero A := {zero := ring0}.
-Instance one_ring2 : One A := {one := ring1}.
-Instance addition_ring2 : Addition A := {addition x y := ring_plus x y}.
-Instance multiplication_ring2 : Multiplication A := {multiplication x y := ring_mult x y}.
-Instance subtraction_ring2 : Subtraction A := {subtraction x y := ring_sub x y}.
-Instance opposite_ring2 : Opposite A := {opposite x := ring_opp x}.
-
-Infix "==" := ring_eq (at level 70, no associativity).
-
-Ltac nsatzA := simpl; unfold Ari; nsatz_domain.
-
-Goal forall x y:A,  x == y -> x+0 == y*1+0.
-nsatzA.
-Qed.
+Context {A:Type}`{Aid:Integral_domain A}.
 
 Lemma example3 : forall x y z,
   x+y+z==0 ->
   x*y+x*z+y*z==0->
-  x*y*z==0 -> x*x*x==0.
+  x*y*z==0 -> x^3%Z==0.
 Proof.
-Time nsatzA. 
-Admitted.
+Time nsatz. 
+Qed.
 
 Lemma example4 : forall x y z u,
   x+y+z+u==0 ->
   x*y+x*z+x*u+y*z+y*u+z*u==0->
   x*y*z+x*y*u+x*z*u+y*z*u==0->
-  x*y*z*u==0 -> x*x*x*x==0.
+  x*y*z*u==0 -> x^4%Z==0.
 Proof.
-Time nsatzA.
+Time nsatz.
 Qed.
 
 Lemma example5 : forall x y z u v,
@@ -53,15 +29,17 @@ Lemma example5 : forall x y z u v,
   x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v==0->
   x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v==0->
   x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z==0 ->
-  x*y*z*u*v==0 -> x*x*x*x*x ==0.
+  x*y*z*u*v==0 -> x^5%Z==0.
 Proof.
-Time nsatzA.
+Time nsatz.
 Qed.
 
 Goal forall x y:Z,  x = y -> (x+0)%Z = (y*1+0)%Z.
 nsatz.
 Qed.
 
+Require Import Reals.
+
 Goal forall x y:R,  x = y -> (x+0)%R = (y*1+0)%R.
 nsatz.
 Qed.
@@ -70,85 +48,17 @@ Goal forall a b c x:R, a = b -> b = c -> (a*a)%R = (c*c)%R.
 nsatz.
 Qed.
 
-Section Examples.
-
-Delimit Scope PE_scope with PE.
-Infix "+" := PEadd : PE_scope.
-Infix "*" := PEmul : PE_scope.
-Infix "-" := PEsub : PE_scope.
-Infix "^" := PEpow : PE_scope.
-Notation "[ n ]" := (@PEc Z n) (at level 0).
-
-Open Scope R_scope.
-
-Lemma example1 : forall x y,
-  x+y=0 ->
-  x*y=0 ->
-  x^2=0.
-Proof.
- nsatz.
-Qed.
-
-Lemma example2 : forall x, x^2=0 -> x=0.
-Proof.
- nsatz.
-Qed.
-
-(*
-Notation X  := (PEX Z 3).
-Notation Y  := (PEX Z 2).
-Notation Z_ := (PEX Z 1).
-*)
-Lemma example3b : forall x y z,
-  x+y+z=0 ->
-  x*y+x*z+y*z=0->
-  x*y*z=0 -> x^3=0.
-Proof.
-Time nsatz. 
-Qed.
-
-(*
-Notation X  := (PEX Z 4).
-Notation Y  := (PEX Z 3).
-Notation Z_ := (PEX Z 2).
-Notation U  := (PEX Z 1).
-*)
-Lemma example4b : forall x y z u,
-  x+y+z+u=0 ->
-  x*y+x*z+x*u+y*z+y*u+z*u=0->
-  x*y*z+x*y*u+x*z*u+y*z*u=0->
-  x*y*z*u=0 -> x^4=0.
-Proof.
-Time nsatz.
-Qed.
-
-(*
-Notation x_ := (PEX Z 5).
-Notation y_ := (PEX Z 4).
-Notation z_ := (PEX Z 3).
-Notation u_ := (PEX Z 2).
-Notation v_ := (PEX Z 1).
-Notation "x :: y" := (List.cons x y)
-(at level 60, right associativity, format "'[hv' x  ::  '/' y ']'").
-Notation "x :: y" := (List.app x y)
-(at level 60, right associativity, format "x :: y").
-*)
-
-Lemma example5b : forall x y z u v,
-  x+y+z+u+v=0 ->
-  x*y+x*z+x*u+x*v+y*z+y*u+y*v+z*u+z*v+u*v=0->
-  x*y*z+x*y*u+x*y*v+x*z*u+x*z*v+x*u*v+y*z*u+y*z*v+y*u*v+z*u*v=0->
-  x*y*z*u+y*z*u*v+z*u*v*x+u*v*x*y+v*x*y*z=0 ->
-  x*y*z*u*v=0 -> x^5=0.
-Proof.
-Time nsatz.
-Qed.
-
-End Examples.
+End test.
 
 Section Geometry.
+(* See the interactive pictures of Laurent Théry 
+   on http://www-sop.inria.fr/marelle/CertiGeo/ 
+   and research paper on 
+   https://docs.google.com/fileview?id=0ByhB3nPmbnjTYzFiZmIyNGMtYTkwNC00NWFiLWJiNzEtODM4NmVkYTc2NTVk&hl=fr
+*)
 
-Open Scope R_scope.
+Require Import List.
+Require Import Reals.
 
 Record point:Type:={
  X:R;
@@ -170,60 +80,122 @@ Definition equal2(A B:point):=
   (X A)=(X B) /\ (Y A)=(Y B).
 
 Definition equal3(A B:point):=
-  ((X A)-(X B))^2+((Y A)-(Y B))^2 = 0.
+  ((X A)-(X B))^2%Z+((Y A)-(Y B))^2%Z = 0.
 
 Definition nequal2(A B:point):=
   (X A)<>(X B) \/ (Y A)<>(Y B).
 
 Definition nequal3(A B:point):=
-  not (((X A)-(X B))^2+((Y A)-(Y B))^2 = 0).
+  not (((X A)-(X B))^2%Z+((Y A)-(Y B))^2%Z = 0).
 
 Definition middle(A B I:point):=
-  2*(X I)=(X A)+(X B) /\ 2*(Y I)=(Y A)+(Y B).
+  2%R*(X I)=(X A)+(X B) /\ 2%R*(Y I)=(Y A)+(Y B).
 
 Definition distance2(A B:point):=
-  (X B - X A)^2 + (Y B - Y A)^2.
+  (X B - X A)^2%Z + (Y B - Y A)^2%Z.
 
 (* AB = CD *)
 Definition samedistance2(A B C D:point):=
-  (X B - X A)^2 + (Y B - Y A)^2 = (X D - X C)^2 + (Y D - Y C)^2.
+  (X B - X A)^2%Z + (Y B - Y A)^2%Z = (X D - X C)^2%Z + (Y D - Y C)^2%Z.
 Definition determinant(A O B:point):=
   (X A - X O)*(Y B - Y O) - (Y A - Y O)*(X B - X O).
 Definition scalarproduct(A O B:point):=
   (X A - X O)*(X B - X O) + (Y A - Y O)*(Y B - Y O).
 Definition norm2(A O B:point):=
-  ((X A - X O)^2+(Y A - Y O)^2)*((X B - X O)^2+(Y B - Y O)^2).
-
-
-Lemma a1:forall A B C:Prop, ((A\/B)/\(A\/C)) -> (A\/(B/\C)).
-intuition.
-Qed.
- 
-Lemma a2:forall A B C:Prop, ((A\/C)/\(B\/C)) -> ((A/\B)\/C).
-intuition.
+  ((X A - X O)^2%Z+(Y A - Y O)^2%Z)*((X B - X O)^2%Z+(Y B - Y O)^2%Z).
+
+Definition equaldistance(A B C D:point):=
+  ((X B) - (X A))^2%Z + ((Y B) - (Y A))^2%Z =
+  ((X D) - (X C))^2%Z + ((Y D) - (Y C))^2%Z.
+
+Definition equaltangente(A B C D E F:point):=
+  let s1:= determinant A B C in
+  let c1:= scalarproduct A B C in
+  let s2:= determinant D E F in
+  let c2:= scalarproduct D E F in
+  s1 * c2 = s2 * c1.
+
+Ltac cnf2 f :=
+  match f with
+   | ?A \/ (?B /\ ?C) =>
+     let c1 := cnf2 (A\/B) in
+     let c2 := cnf2 (A\/C) in constr:(c1/\c2)
+   | (?B /\ ?C) \/ ?A =>
+     let c1 := cnf2 (B\/A) in
+     let c2 := cnf2 (C\/A) in constr:(c1/\c2)
+   | (?A \/ ?B) \/ ?C =>
+     let c1 := cnf2 (B\/C) in cnf2 (A \/ c1)
+   | _ => f
+  end
+with cnf f :=
+  match f with
+   | ?A \/ ?B =>
+     let c1 := cnf A in
+       let c2 := cnf B in
+         cnf2 (c1 \/ c2)
+   | ?A /\ ?B =>
+     let c1 := cnf A in
+       let c2 := cnf B in
+         constr:(c1 /\ c2)
+   | _ => f
+  end.
+      
+Ltac scnf :=
+  match goal with
+    | |- ?f => let c := cnf f in
+      assert c;[repeat split| tauto]
+  end.
+
+Ltac disj_to_pol f :=
+  match f with
+   | ?a = ?b \/ ?g => let p := disj_to_pol g in constr:((a - b)* p)
+   | ?a = ?b => constr:(a - b)
+  end.
+
+Lemma fastnsatz1:forall x y:R, x - y = 0 -> x = y.
+nsatz.
 Qed.
 
-Lemma a3:forall a b c d:R, (a-b)*(c-d)=0 -> (a=b \/ c=d).
-intros.
-assert ( (a-b = 0) \/ (c-d = 0)).
-apply Rmult_integral.
-trivial.
-destruct H0.
-left; nsatz.
-right; nsatz.
-Qed.
+Ltac fastnsatz:=
+  try trivial; try apply fastnsatz1; try trivial; nsatz.
+  
+Ltac proof_pol_disj :=
+  match goal with
+   | |- ?g => let p := disj_to_pol g in
+     let h := fresh "hp" in
+     assert (h:p = 0);
+     [idtac|
+      prod_disj h p]
+   | _ => idtac
+  end
+with prod_disj h p :=
+  match goal with
+   | |- ?a = ?b \/ ?g => 
+        match p with
+          | ?q * ?p1 => 
+        let h0 := fresh "hp" in
+        let h1 := fresh "hp" in
+        let h2 := fresh "hp" in
+        assert (h0:a - b = 0 \/ p1 = 0);
+        [apply Rmult_integral; exact h|
+         destruct h0 as [h1|h2];
+         [left; fastnsatz|
+          right; prod_disj h2 p1]]
+        end
+   | _ => fastnsatz
+  end.
 
-Ltac geo_unfold :=
-  unfold collinear; unfold parallel; unfold notparallel; unfold orthogonal;
-  unfold equal2; unfold equal3; unfold nequal2; unfold nequal3; 
-  unfold middle; unfold samedistance2; 
-  unfold determinant; unfold scalarproduct; unfold norm2; unfold distance2.
+(*
+Goal forall a b c d e f:R, a=b \/ c=d \/ e=f \/ e=a.
+intros. scnf; proof_pol_disj .
+admit.*)
 
-Ltac geo_end :=
-  repeat (
-  repeat (match goal with h:_/\_ |- _ => decompose [and] h; clear h end);
-  repeat (apply a1 || apply a2 || apply a3);
-  repeat split).
+Ltac geo_unfold :=
+  unfold collinear, parallel, notparallel, orthogonal,
+    equal2, equal3, nequal2, nequal3,
+    middle, samedistance2,
+    determinant, scalarproduct, norm2, distance2,
+      equaltangente, determinant, scalarproduct, equaldistance.
 
 Ltac geo_rewrite_hyps:=
   repeat (match goal with
@@ -231,14 +203,41 @@ Ltac geo_rewrite_hyps:=
            | h:Y _ = _ |- _ => rewrite h in *; clear h
           end).
 
+Ltac geo_split_hyps:=
+  repeat (match goal with
+           | h:_ /\ _ |- _ => destruct h
+          end).
+
 Ltac geo_begin:=
   geo_unfold;
   intros;
   geo_rewrite_hyps;
-  geo_end.
+  geo_split_hyps;
+  scnf; proof_pol_disj.
 
 (* Examples *)
 
+Lemma medians: forall A B C A1 B1 C1 H:point,
+  middle B C A1 ->  
+  middle A C B1 -> 
+  middle A B C1 -> 
+  collinear A A1 H -> collinear B B1 H -> 
+  collinear C C1 H
+  \/ collinear A B C.
+Proof. geo_begin.
+idtac "Medians".
+ Time nsatz.
+(*Finished transaction in 2. secs (2.69359u,0.s)
+*) Qed.
+
+Lemma Pythagore: forall A B C:point,
+  orthogonal A B A C ->
+  distance2 A C + distance2 A B = distance2 B C.
+Proof. geo_begin.
+idtac "Pythagore". 
+Time nsatz.
+(*Finished transaction in 0. secs (0.354946u,0.s)
+*) Qed.
 
 Lemma Thales: forall O A B C D:point,
   collinear O A C -> collinear O B D ->
@@ -246,9 +245,268 @@ Lemma Thales: forall O A B C D:point,
   (distance2 O B * distance2 O C = distance2 O D * distance2 O A
   /\ distance2 O B * distance2 C D = distance2 O D * distance2 A B)
  \/ collinear O A B.
-repeat geo_begin.
+geo_begin.
+idtac "Thales".
+Time nsatz. (*Finished transaction in 2. secs (1.598757u,0.s)*)
+Time nsatz.
+Qed.
+
+Lemma segments_of_chords: forall A B C D M O:point,
+  equaldistance O A O B ->
+  equaldistance O A O C ->
+  equaldistance O A O D ->
+  collinear A B M ->
+  collinear C D M ->
+  (distance2 M A) * (distance2 M B) = (distance2 M C) * (distance2 M D)
+  \/ parallel A B C D.
+Proof. 
+geo_begin. 
+idtac "segments_of_chords".
+Time nsatz.
+(*Finished transaction in 3. secs (2.704589u,0.s)
+*) Qed.
+
+
+Lemma isoceles: forall A B C:point,
+  equaltangente A B C B C A ->
+  distance2 A B = distance2 A C
+  \/ collinear A B C.
+Proof. geo_begin.  Time nsatz. 
+(*Finished transaction in 1. secs (1.140827u,0.s)*) Qed.
+
+Lemma minh: forall A B C D O E H I:point,
+  X A = 0 -> Y A = 0 -> Y O = 0 ->
+  equaldistance O A O B -> 
+  equaldistance O A O C ->
+  equaldistance O A O D ->
+  orthogonal A C B D ->
+  collinear A C E ->
+  collinear B D E ->
+  collinear A B H ->
+  orthogonal E H A B ->
+  collinear C D I ->
+  middle C D I ->
+  collinear H E I
+  \/ (X C)^2%Z * (X B)^5%Z * (X O)^2%Z
+     * (X C - 2%Z * X O)^3%Z * (-2%Z * X O + X B)=0
+  \/  parallel A C B D.
+Proof. geo_begin.
+idtac "minh". 
+Time nsatz with radicalmax :=1%N strategy:=1%Z
+  parameters:=(X O::X B::X C::nil)
+  variables:= (@nil R).
+(*Finished transaction in 13. secs (10.102464u,0.s)
+*)
+Qed.
+
+Lemma Pappus: forall A B C A1 B1 C1 P Q S:point,
+  X A = 0 -> Y A = 0 -> Y B = 0 -> Y C = 0 -> 
+  collinear A1 B1 C1 ->
+  collinear A B1 P -> collinear A1 B P ->
+  collinear A C1 Q -> collinear A1 C Q ->
+  collinear B C1 S -> collinear B1 C S ->
+  collinear P Q S 
+  \/ (Y A1 - Y B1)^2%Z=0 \/ (X A = X B1)
+  \/ (X A1 = X C) \/ (X C = X B1)
+  \/ parallel A B1 A1 B \/ parallel A C1 A1 C \/ parallel B C1 B1 C.
+Proof.
+geo_begin.
+idtac "Pappus".
+Time nsatz with radicalmax :=1%N strategy:=0%Z
+  parameters:=(X B::X A1::Y A1::X B1::Y B1::X C::Y C1::nil)
+  variables:= (X B
+ :: X A1
+    :: Y A1
+       :: X B1
+          :: Y B1
+             :: X C
+                :: Y C1
+                   :: X C1 :: Y P :: X P :: Y Q :: X Q :: Y S :: X S :: nil).
+(*Finished transaction in 8. secs (7.795815u,0.000999999999999s)
+*)
+Qed.
+
+Lemma Simson: forall A B C O D E F G:point,
+  X A = 0 -> Y A = 0 -> 
+  equaldistance O A O B ->
+  equaldistance O A O C ->
+  equaldistance O A O D ->
+  orthogonal  E D B C ->
+  collinear B C E ->
+  orthogonal F D A C ->
+  collinear A C F ->
+  orthogonal G D A B ->
+  collinear A B G ->
+  collinear E F G
+  \/ (X C)^2%Z = 0 \/ (Y C)^2%Z = 0 \/ (X B)^2%Z = 0 \/ (Y B)^2%Z = 0 \/ (Y C - Y B)^2%Z = 0
+  \/ equal3 B A 
+  \/ equal3 A C \/ (X C - X B)^2%Z = 0
+  \/ equal3 B C.
+Proof.
+geo_begin.
+idtac "Simson".
+Time nsatz with radicalmax :=1%N strategy:=0%Z
+  parameters:=(X B::Y B::X C::Y C::Y D::nil)
+  variables:= (@nil R). (* compute -[X Y]. *)
+(*Finished transaction in 8. secs (7.550852u,0.s)
+*)
+Qed.
+
+Lemma threepoints: forall A B C A1 B1 A2 B2 H1 H2 H3:point,
+  (* H1 intersection of bisections *)
+  middle B C A1 ->  orthogonal H1 A1 B C ->
+  middle A C B1 -> orthogonal H1 B1 A C -> 
+  (* H2 intersection of medians *)
+  collinear A A1 H2 -> collinear B B1 H2 -> 
+  (* H3 intersection of altitudes *)
+  collinear B C A2 ->  orthogonal A A2 B C ->
+  collinear A C B2 -> orthogonal B B2 A C ->
+  collinear A A1 H3 -> collinear B B1 H3 -> 
+  collinear H1 H2 H3
+  \/ collinear A B C.
+Proof. geo_begin. 
+idtac "threepoints".
+Time nsatz. 
+(*Finished transaction in 7. secs (6.282045u,0.s)
+*) Qed.
+
+Lemma Feuerbach:  forall A B C A1 B1 C1 O A2 B2 C2 O2:point, 
+  forall r r2:R,
+  X A = 0 -> Y A =  0 -> X B = 1 -> Y B =  0->
+  middle A B C1 -> middle B C A1 -> middle C A B1 ->
+  distance2 O A1 = distance2 O B1 ->
+  distance2 O A1 = distance2 O C1 ->
+  collinear A B C2 -> orthogonal A B O2 C2 -> 
+  collinear B C A2 -> orthogonal B C O2 A2 ->
+  collinear A C B2 -> orthogonal A C O2 B2 ->
+  distance2 O2 A2 = distance2 O2 B2 ->
+  distance2 O2 A2 = distance2 O2 C2 ->
+  r^2%Z = distance2 O A1 ->
+  r2^2%Z = distance2 O2 A2 ->
+  distance2 O O2 = (r + r2)^2%Z
+  \/ distance2 O O2 = (r - r2)^2%Z
+  \/ collinear A B C.
+Proof. geo_begin. 
+idtac "Feuerbach".
+Time nsatz. 
+(*Finished transaction in 21. secs (19.021109u,0.s)*)
+Qed.
+
+
+
+
+Lemma Euler_circle: forall A B C A1 B1 C1 A2 B2 C2 O:point,
+  middle A B C1 -> middle B C A1 -> middle C A B1 ->
+  orthogonal A B C C2 -> collinear A B C2 ->
+  orthogonal B C A A2 -> collinear B C A2 ->
+  orthogonal A C B B2 -> collinear A C B2 ->
+  distance2 O A1 = distance2 O B1 ->
+  distance2 O A1 = distance2 O C1 ->
+  (distance2 O A2 = distance2 O A1
+   /\distance2 O B2 = distance2 O A1
+   /\distance2 O C2 = distance2 O A1)
+  \/ collinear A B C.
+Proof. geo_begin. 
+idtac "Euler_circle 3 goals".
+Time nsatz. 
+(*Finished transaction in 13. secs (11.208296u,0.124981s)*)
+Time nsatz.  
+(*Finished transaction in 10. secs (8.846655u,0.s)*) 
+Time nsatz. 
+(*Finished transaction in 11. secs (9.186603u,0.s)*)
+Qed.
+
+
+
+Lemma Desargues: forall A B C A1 B1 C1 P Q R S:point,
+  X S = 0 -> Y S = 0 -> Y A = 0 ->
+  collinear A S A1 -> collinear B S B1 -> collinear C S C1 ->
+  collinear B1 C1 P -> collinear B C P ->
+  collinear A1 C1 Q -> collinear A C Q -> 
+  collinear A1 B1 R -> collinear A B R ->
+  collinear P Q R
+  \/ X A = X B \/ X A = X C \/ X B = X C  \/ X A = 0 \/ Y B = 0 \/ Y C = 0
+  \/ collinear S B C \/ parallel A C A1 C1 \/ parallel A B A1 B1.
+Proof.
+geo_begin.
+idtac "Desargues".
+Time 
+let lv := rev (X A
+ :: X B
+    :: Y B
+       :: X C
+          :: Y C
+             :: Y A1 :: X A1
+                :: Y B1
+                   :: Y C1
+                      :: X R
+                         :: Y R
+                            :: X Q
+                               :: Y Q :: X P :: Y P :: X C1 :: X B1 :: nil) in
+nsatz with radicalmax :=1%N strategy:=0%Z
+  parameters:=(X A::X B::Y B::X C::Y C::X A1::Y B1::Y C1::nil)
+  variables:= lv. (*Finished transaction in 8. secs (8.02578u,0.001s)*)
+Qed.
+
+Lemma chords: forall O A B C D M:point,
+  equaldistance O A O B ->
+  equaldistance O A O C ->
+  equaldistance O A O D ->
+  collinear A B M -> collinear C D M ->
+  scalarproduct A M B = scalarproduct C M D
+  \/ parallel A B C D.
+Proof. geo_begin. 
+idtac "chords".
+ Time nsatz. 
+(*Finished transaction in 4. secs (3.959398u,0.s)*)
+Qed.
+
+Lemma Ceva: forall A B C D E F M:point,
+  collinear M A D -> collinear M B E -> collinear M C F ->
+  collinear B C D -> collinear E A C -> collinear F A B ->
+  (distance2 D B) * (distance2 E C) * (distance2 F A) =
+  (distance2 D C) * (distance2 E A) * (distance2 F B)
+  \/ collinear A B C.
+Proof. geo_begin. 
+idtac "Ceva".
 Time nsatz.
+(*Finished transaction in 105. secs (104.121171u,0.474928s)*)
+Qed.
+
+Lemma bissectrices: forall A B C M:point,
+  equaltangente C A M M A B ->
+  equaltangente A B M M B C ->
+  equaltangente B C M M C A
+  \/ equal3 A B.
+Proof. geo_begin. 
+idtac "bissectrices".
 Time nsatz.
+(*Finished transaction in 2. secs (1.937705u,0.s)*)
+Qed.
+
+Lemma bisections: forall A B C A1 B1 C1 H:point,
+  middle B C A1 ->  orthogonal H A1 B C ->
+  middle A C B1 -> orthogonal H B1 A C -> 
+  middle A B C1 -> 
+  orthogonal H C1 A B 
+  \/ collinear A B C.
+Proof. geo_begin.
+idtac "bisections". 
+Time nsatz. (*Finished transaction in 2. secs (2.024692u,0.002s)*)
+Qed.
+
+Lemma altitudes: forall A B C A1 B1 C1 H:point,
+  collinear B C A1 ->  orthogonal A A1 B C ->
+  collinear A C B1 -> orthogonal B B1 A C -> 
+  collinear A B C1 -> orthogonal C C1 A B ->
+  collinear A A1 H -> collinear B B1 H -> 
+  collinear C C1 H
+  \/ equal2 A B
+  \/ collinear A B C.
+Proof. geo_begin.
+idtac "altitudes".
+Time nsatz. (*Finished transaction in 3. secs (3.001544u,0.s)*)
+Time nsatz. (*Finished transaction in 4. secs (3.113527u,0.s)*)
 Qed.
 
 Lemma hauteurs:forall A B C A1 B1 C1 H:point,
@@ -261,26 +519,16 @@ Lemma hauteurs:forall A B C A1 B1 C1 H:point,
   \/ collinear A B C.
 
 geo_begin.
- 
-(* Time nsatzRpv 2%N 1%Z (@nil R) (@nil R).*)
-(*Finished transaction in 3. secs (2.363641u,0.s)*)
-(*Time nsatz_domainR. trop long! *)
+idtac "hauteurs".
 Time 
  let lv := constr:(Y A1
- :: X A1
-    :: Y B1
-       :: X B1
-          :: Y A0
-             :: Y B
-                :: X B
-                   :: X A0
-                      :: X H
-                         :: Y C
-                            :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in
- nsatz_domainpv ltac:pretacR 2%N 1%Z (@Datatypes.nil R) lv ltac:simplR Rdi;
-  discrR.
-(* Finished transaction in 6. secs (5.579152u,0.001s) *)
+ :: X A1 :: Y B1 :: X B1 :: Y A :: Y B :: X B :: X A :: X H :: Y C
+ :: Y C1 :: Y H :: X C1 :: X C :: (@Datatypes.nil R)) in
+nsatz with radicalmax := 2%N strategy := 1%Z parameters := (@Datatypes.nil R)
+ variables := lv.
+(*Finished transaction in 5. secs (4.360337u,0.008999s)*)
 Qed.
 
+
 End Geometry.
 
diff --git a/test-suite/success/PCase.v b/test-suite/success/PCase.v
new file mode 100644
index 00000000..67d680ba
--- /dev/null
+++ b/test-suite/success/PCase.v
@@ -0,0 +1,66 @@
+
+(** Some tests of patterns containing matchs ending with joker branches.
+    Cf. the new form of the [constr_pattern] constructor [PCase]
+    in [pretyping/pattern.ml] *)
+
+(* A universal match matcher *)
+
+Ltac kill_match :=
+ match goal with
+   |- context [ match ?x with _ => _ end ] => destruct x
+ end.
+
+(* A match matcher restricted to a given type : nat *)
+
+Ltac kill_match_nat :=
+ match goal with
+   |- context [ match ?x in nat with _ => _ end ] => destruct x
+ end.
+
+(* Another way to restrict to a given type : give a branch *)
+
+Ltac kill_match_nat2 :=
+ match goal with
+   |- context [ match ?x with S _ => _ | _ => _ end ] => destruct x
+ end.
+
+(* This should act only on empty match *)
+
+Ltac kill_match_empty :=
+ match goal with
+   |- context [ match ?x with end ] => destruct x
+ end.
+
+Lemma test1 (b:bool) : if b then True else O=O.
+Proof.
+ Fail kill_match_nat.
+ Fail kill_match_nat2.
+ Fail kill_match_empty.
+ kill_match. exact I. exact eq_refl.
+Qed.
+
+Lemma test2a (n:nat) : match n with O => True | S n => (n = n) end.
+Proof.
+ Fail kill_match_empty.
+ kill_match_nat. exact I. exact eq_refl.
+Qed.
+
+Lemma test2b (n:nat) : match n with O => True | S n => (n = n) end.
+Proof.
+ kill_match_nat2. exact I. exact eq_refl.
+Qed.
+
+Lemma test2c (n:nat) : match n with O => True | S n => (n = n) end.
+Proof.
+ kill_match. exact I. exact eq_refl.
+Qed.
+
+Lemma test3a (f:False) : match f return Prop with end.
+Proof.
+ kill_match_empty.
+Qed.
+
+Lemma test3b (f:False) : match f return Prop with end.
+Proof.
+ kill_match.
+Qed.
diff --git a/test-suite/success/PrintSortedUniverses.v b/test-suite/success/PrintSortedUniverses.v
new file mode 100644
index 00000000..81326580
--- /dev/null
+++ b/test-suite/success/PrintSortedUniverses.v
@@ -0,0 +1,2 @@
+Require Reals.
+Print Sorted Universes.
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index 81bdbc29..00a13aed 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -1,3 +1,9 @@
+(* Before loading Program, check non-anomaly on missing library Program *)
+
+Fail Program Definition f n (e:n=n): {n|n=0} := match n,e with 0, refl => 0 | _, _ => 0 end.
+
+(* Then we test Program properly speaking *)
+
 Require Import Arith Program.
 Require Import ZArith Zwf.
 
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index d4e6a82e..2602c7e3 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -55,13 +55,13 @@ Check (cons 3 (cons 2 nil)).
 
 Require Import Bvector.
 
-Print vector.
+Print Vector.t.
 
-Check (Vnil nat).
+Check (Vector.nil nat).
 
-Check (fun (A:Set)(a:A)=> Vcons _ a _ (Vnil _)).
+Check (fun (A:Set)(a:A)=> Vector.cons _ a _ (Vector.nil _)).
 
-Check (Vcons _ 5 _ (Vcons _ 3 _ (Vnil _))).
+Check (Vector.cons _ 5 _ (Vector.cons _ 3 _ (Vector.nil _))).
 
 
 
@@ -315,16 +315,16 @@ Proof.
 Qed.
 
 Definition Vtail_total
-   (A : Set) (n : nat) (v : vector A n) : vector A (pred n):=
-match v in (vector _ n0) return (vector A (pred n0)) with
-| Vnil => Vnil A
-| Vcons _ n0 v0 => v0
+   (A : Set) (n : nat) (v : Vector.t A n) : Vector.t A (pred n):=
+match v in (Vector.t _ n0) return (Vector.t A (pred n0)) with
+| Vector.nil => Vector.nil A
+| Vector.cons _ n0 v0 => v0
 end.
 
-Definition Vtail' (A:Set)(n:nat)(v:vector A n) : vector A (pred n).
+Definition Vtail' (A:Set)(n:nat)(v:Vector.t A n) : Vector.t A (pred n).
  case v.
  simpl.
- exact (Vnil A).
+ exact (Vector.nil A).
  simpl.
  auto.
 Defined.
@@ -543,7 +543,7 @@ Inductive ex_Set  (P : Set -> Prop) : Type :=
 Inductive comes_from_the_left (P Q:Prop): P \/ Q -> Prop :=
   c1 : forall p, comes_from_the_left P Q (or_introl (A:=P) Q p).
 
-Goal (comes_from_the_left _ _ (or_introl  True I)).
+Goal (comes_from_the_left _ _ (or_introl True I)).
 split.
 Qed.
 
@@ -966,37 +966,37 @@ let rec div_aux x y =
            | Right -> div_aux (minus x y) y)
 *)
 
-Lemma vector0_is_vnil : forall (A:Set)(v:vector A 0), v = Vnil A.
+Lemma vector0_is_vnil : forall (A:Set)(v:Vector.t A 0), v = Vector.nil A.
 Proof.
  intros A v;inversion v.
 Abort.
 
 (*
- Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),
+ Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),
                                   n= 0 -> v = Vnil A.
 
 Toplevel input, characters 40281-40287
-> Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),                                    n= 0 -> v = Vnil A.
+> Lemma Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),                                    n= 0 -> v = Vnil A.
 >                                                                                                                 ^^^^^^
 Error: In environment
 A : Set
 n : nat
-v : vector A n
+v : Vector.t A n
 e : n = 0
-The term "Vnil A" has type "vector A 0" while it is expected to have type
- "vector A n"
+The term "Vnil A" has type "Vector.t A 0" while it is expected to have type
+ "Vector.t A n"
 *)
  Require Import JMeq.
 
-Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:vector A n),
-                                  n= 0 -> JMeq v (Vnil A).
+Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),
+                                  n= 0 -> JMeq v (Vector.nil A).
 Proof.
  destruct v.
  auto.
  intro; discriminate.
 Qed.
 
-Lemma vector0_is_vnil : forall (A:Set)(v:vector A 0), v = Vnil A.
+Lemma vector0_is_vnil : forall (A:Set)(v:Vector.t A 0), v = Vector.nil A.
 Proof.
  intros a v;apply JMeq_eq.
  apply vector0_is_vnil_aux.
@@ -1004,56 +1004,56 @@ Proof.
 Qed.
 
 
-Implicit Arguments Vcons [A n].
-Implicit Arguments Vnil [A].
-Implicit Arguments Vhead [A n].
-Implicit Arguments Vtail [A n].
+Implicit Arguments Vector.cons [A n].
+Implicit Arguments Vector.nil [A].
+Implicit Arguments Vector.hd [A n].
+Implicit Arguments Vector.tl [A n].
 
-Definition Vid : forall (A : Type)(n:nat), vector A n -> vector A n.
+Definition Vid : forall (A : Type)(n:nat), Vector.t A n -> Vector.t A n.
 Proof.
  destruct n; intro v.
- exact Vnil.
- exact (Vcons  (Vhead v) (Vtail v)).
+ exact Vector.nil.
+ exact (Vector.cons  (Vector.hd v) (Vector.tl v)).
 Defined.
 
-Eval simpl in (fun (A:Set)(v:vector A 0) => (Vid _ _ v)).
+Eval simpl in (fun (A:Set)(v:Vector.t A 0) => (Vid _ _ v)).
 
-Eval simpl in (fun (A:Set)(v:vector A 0) => v).
+Eval simpl in (fun (A:Set)(v:Vector.t A 0) => v).
 
 
 
-Lemma Vid_eq : forall (n:nat) (A:Type)(v:vector A n), v=(Vid _ n v).
+Lemma Vid_eq : forall (n:nat) (A:Type)(v:Vector.t A n), v=(Vid _ n v).
 Proof.
  destruct v.
  reflexivity.
  reflexivity.
 Defined.
 
-Theorem zero_nil : forall A (v:vector A 0), v = Vnil.
+Theorem zero_nil : forall A (v:Vector.t A 0), v = Vector.nil.
 Proof.
  intros.
- change (Vnil (A:=A)) with (Vid _ 0 v).
+ change (Vector.nil (A:=A)) with (Vid _ 0 v).
  apply Vid_eq.
 Defined.
 
 
 Theorem decomp :
-  forall (A : Set) (n : nat) (v : vector A (S n)),
-  v = Vcons (Vhead v) (Vtail v).
+  forall (A : Set) (n : nat) (v : Vector.t A (S n)),
+  v = Vector.cons (Vector.hd v) (Vector.tl v).
 Proof.
  intros.
- change (Vcons (Vhead v) (Vtail v)) with (Vid _  (S n) v).
+ change (Vector.cons (Vector.hd v) (Vector.tl v)) with (Vid _  (S n) v).
  apply Vid_eq.
 Defined.
 
 
 
 Definition vector_double_rect :
-    forall (A:Set) (P: forall (n:nat),(vector A n)->(vector A n) -> Type),
-        P 0 Vnil Vnil ->
-        (forall n (v1 v2 : vector A n) a b, P n v1 v2 ->
-             P (S n) (Vcons a v1) (Vcons  b v2)) ->
-        forall n (v1 v2 : vector A n), P n v1 v2.
+    forall (A:Set) (P: forall (n:nat),(Vector.t A n)->(Vector.t A n) -> Type),
+        P 0 Vector.nil Vector.nil ->
+        (forall n (v1 v2 : Vector.t A n) a b, P n v1 v2 ->
+             P (S n) (Vector.cons a v1) (Vector.cons  b v2)) ->
+        forall n (v1 v2 : Vector.t A n), P n v1 v2.
  induction n.
  intros; rewrite (zero_nil _ v1); rewrite (zero_nil _ v2).
  auto.
@@ -1063,24 +1063,24 @@ Defined.
 
 Require Import Bool.
 
-Definition bitwise_or n v1 v2 : vector bool n :=
-   vector_double_rect bool  (fun n v1 v2 => vector bool n)
-                        Vnil
-                        (fun n v1 v2 a b r => Vcons (orb a b) r) n v1 v2.
+Definition bitwise_or n v1 v2 : Vector.t bool n :=
+   vector_double_rect bool  (fun n v1 v2 => Vector.t bool n)
+                        Vector.nil
+                        (fun n v1 v2 a b r => Vector.cons (orb a b) r) n v1 v2.
 
 
-Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:vector A p){struct v}
+Fixpoint vector_nth (A:Set)(n:nat)(p:nat)(v:Vector.t A p){struct v}
                   : option A :=
   match n,v  with
-    _   , Vnil => None
-  | 0   , Vcons b  _ _ => Some b
-  | S n', Vcons _  p' v' => vector_nth A n'  p' v'
+    _   , Vector.nil => None
+  | 0   , Vector.cons b  _ _ => Some b
+  | S n', Vector.cons _  p' v' => vector_nth A n'  p' v'
   end.
 
 Implicit Arguments vector_nth [A p].
 
 
-Lemma nth_bitwise : forall (n:nat) (v1 v2: vector bool n) i  a b,
+Lemma nth_bitwise : forall (n:nat) (v1 v2: Vector.t bool n) i  a b,
       vector_nth i v1 = Some a ->
       vector_nth i v2 = Some b ->
       vector_nth i (bitwise_or _ v1 v2) = Some (orb a b).
diff --git a/test-suite/success/Scheme.v b/test-suite/success/Scheme.v
new file mode 100644
index 00000000..dd5aa81d
--- /dev/null
+++ b/test-suite/success/Scheme.v
@@ -0,0 +1,4 @@
+(* This failed in 8.3pl2 *)
+
+Scheme Induction for eq Sort Prop.
+Check eq_ind_dep.
diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index 324d340a..c4e67677 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: Tauto.v 14641 2011-11-06 11:59:10Z herbelin $ *)
-
 (**** Tactics Tauto and Intuition ****)
 
 (**** Tauto:
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index 6cc443bb..705bdc45 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index a6f9fa23..e3183ef2 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -202,6 +202,13 @@ try apply H.
 unfold ID; apply H0.
 Qed.
 
+(* Test hyp in "apply -> ... in hyp" is correctly instantiated by Ltac *)
+
+Goal (True <-> False) -> True -> False.
+intros Heq H.
+match goal with [ H : True |- _ ] => apply -> Heq in H end.
+Abort.
+
 (* Test coercion below product and on non meta-free terms in with bindings *)
 (* Cf wishes #1408 from E. Makarov *)
 
@@ -326,13 +333,12 @@ exact (refl_equal 4).
 Qed.
 
 (* From 12612, descent in conjunctions is more powerful *)
-(* The following, which was failing badly in bug 1980, is now accepted
-   (even if somehow surprising) *)
+(* The following, which was failing badly in bug 1980, is now
+   properly rejected, as descend in conjunctions builds an
+   ill-formed elimination from Prop to Type. *)
 
 Goal True.
-eapply ex_intro.
-instantiate (2:=fun _ :True => True).
-instantiate (1:=I).
+Fail eapply ex_intro.
 exact I.
 Qed.
 
@@ -391,3 +397,21 @@ intro x;
 apply x.
 
 *)
+
+Section A.
+
+Variable map : forall (T1 T2 : Type) (f : T1 -> T2) (t11 t12 : T1),
+  identity (f t11) (f t12).
+
+Variable mapfuncomp : forall (X Y Z : Type) (f : X -> Y) (g : Y -> Z) (x x' : X),
+  identity (map Y Z g (f x) (f x')) (map X Z (fun x0 : X => g (f x0)) x x').
+
+Goal forall X:Type, forall Y:Type, forall f:X->Y, forall x : X, forall x' : X, 
+  forall g : Y -> X,
+  let gf := (fun x : X => g (f x)) : X -> X in
+   identity (map Y X g (f x) (f x')) (map X X gf x x').
+intros.
+apply mapfuncomp.
+Abort.
+
+End A.
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
new file mode 100644
index 00000000..9b691e25
--- /dev/null
+++ b/test-suite/success/auto.v
@@ -0,0 +1,26 @@
+(* Wish #2154 by E. van der Weegen *)
+
+(* auto was not using f_equal-style lemmas with metavariables occuring
+   only in the type of an evar of the concl, but not directly in the
+   concl itself *)
+
+Parameters
+  (F: Prop -> Prop)
+  (G: forall T, (T -> Prop) -> Type)
+  (L: forall A (P: A -> Prop), G A P -> forall x, F (P x))
+  (Q: unit -> Prop).
+
+Hint Resolve L.
+
+Goal G unit Q -> F (Q tt).
+  intro.
+  auto.
+Qed.
+
+(* Test implicit arguments in "using" clause *)
+
+Goal forall n:nat, nat * nat.
+auto using (pair O).
+Undo.
+eauto using (pair O).
+Qed.
diff --git a/test-suite/success/autorewritein.v b/test-suite/success/autorewrite.v
index 68f2f7ce..5e9064f8 100644
--- a/test-suite/success/autorewritein.v
+++ b/test-suite/success/autorewrite.v
@@ -19,5 +19,11 @@ Proof.
     apply H;reflexivity.
 Qed.
 
+(* Check autorewrite does not solve existing evars *)
+(* See discussion started by A. Chargueraud in Oct 2010 on coqdev *)
 
+Hint Rewrite <- plus_n_O : base1.
+Goal forall y, exists x, y+x = y.
+eexists. autorewrite with base1.
+Fail reflexivity.
 
diff --git a/test-suite/success/bullet.v b/test-suite/success/bullet.v
new file mode 100644
index 00000000..1099f3e1
--- /dev/null
+++ b/test-suite/success/bullet.v
@@ -0,0 +1,5 @@
+Goal True /\ True.
+split.
+- exact I.
+- exact I.
+Qed.
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index 5ac6ce82..c65cf303 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -30,3 +30,11 @@ change 3 at 1 with (1+2) in H |- *.
 change 3 at 1 with (1+2) in H, H|-.
 change 3 in |- * at 1.
  *)
+
+(* Test that pretyping checks allowed elimination sorts *)
+
+Goal True.
+Fail change True with (let (x,a) := ex_intro _ True (eq_refl True) in x).
+Fail change True with
+        match ex_intro _ True (eq_refl True) with ex_intro x _ => x end.
+Abort.
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index 908b5f77..001beae7 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -81,3 +81,11 @@ Coercion irrelevent := (fun _ => I) : True -> car (Build_Setoid True).
 
 Definition ClaimB := forall (X Y:Setoid) (f: extSetoid X Y) (x:X), f x= f x.
 
+(* Check that coercions are made visible only when modules are imported *)
+
+Module A.
+  Module B. Coercion b2n (b:bool) := if b then 0 else 1. End B.
+  Fail Check S true.
+End A.
+Import A.
+Fail Check S true.
diff --git a/test-suite/success/conv_pbs.v b/test-suite/success/conv_pbs.v
index f6ebacae..05d2c98f 100644
--- a/test-suite/success/conv_pbs.v
+++ b/test-suite/success/conv_pbs.v
@@ -221,3 +221,8 @@ with universal_completeness_stoup (Gamma:context)(A:formula){struct A}
           (ProofForallL x t (subst_formula (remove_assoc _ x rho) A)
           (eq_rect _ (fun D => Gamma'' ; D |- C) p _ (subst_commute _ _ _ _)))))
   end.
+
+
+(* A simple example that raised an uncaught exception at some point *)
+
+Fail Check fun x => @eq_refl x <: true = true.
diff --git a/test-suite/success/destruct.v b/test-suite/success/destruct.v
index 8013e1d3..fc40ea96 100644
--- a/test-suite/success/destruct.v
+++ b/test-suite/success/destruct.v
@@ -74,3 +74,22 @@ destruct H.
 destruct H0.
 reflexivity.
 Qed.
+
+(* These did not work before 8.4 *)
+
+Goal (exists x, x=0) -> True.
+destruct 1 as (_,_); exact I.
+Abort.
+
+Goal (exists x, x=0 /\ True) -> True.
+destruct 1 as (_,(_,H)); exact H.
+Abort.
+
+Goal (exists x, x=0 /\ True) -> True.
+destruct 1 as (_,(_,x)); exact x.
+Abort.
+
+Goal let T:=nat in forall (x:nat) (g:T -> nat), g x = 0.
+intros.
+destruct (g _). (* This was failing in at least r14571 *)
+Abort.
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index 1862ad10..a94d8b1d 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v
index ff880d00..8c00583e 100644
--- a/test-suite/success/eqdecide.v
+++ b/test-suite/success/eqdecide.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -16,12 +16,7 @@ Qed.
 
 Lemma lem2 : forall x y : T, {x = y} + {x <> y}.
 intros x y.
- decide equality x y.
-Qed.
-
-Lemma lem3 : forall x y : T, {x = y} + {x <> y}.
-intros x y.
- decide equality y x.
+ decide equality.
 Qed.
 
 Lemma lem4 : forall x y : T, {x = y} + {x <> y}.
diff --git a/test-suite/success/eta.v b/test-suite/success/eta.v
new file mode 100644
index 00000000..08078012
--- /dev/null
+++ b/test-suite/success/eta.v
@@ -0,0 +1,19 @@
+(* Kernel test (head term is a constant) *)
+Check (fun a : S = S => a : S = fun x => S x).
+
+(* Kernel test (head term is a variable) *)
+Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => f x).
+
+(* Test type inference  (head term is syntactically rigid) *)
+Check (fun (a : list = list) => a : list = fun A => _ A).
+
+(* Test type inference (head term is a variable) *)
+(* This one is still to be done...
+Check (fun (f:nat->nat) (a : f = f) => a : f = fun x => _ x).
+*)
+
+(* Test tactic unification *)
+Goal (forall f:nat->nat, (fun x => f x) = (fun x => f x)) -> S = S.
+intro H; apply H.
+Qed.
+
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 6423ad14..2f1ec757 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -238,3 +238,74 @@ eapply f_equal with (* should fail because ill-typed *)
         end) in H
 || injection H.
 Abort.
+
+(* A legitimate simple eapply that was failing in coq <= 8.3.
+   Cf. in Unification.w_merge the addition of an extra pose_all_metas_as_evars
+   on 30/9/2010
+*)
+
+Lemma simple_eapply_was_failing :
+ (forall f:nat->nat, exists g, f = g) -> True.
+Proof.
+ assert (modusponens : forall P Q, P -> (P->Q) -> Q) by auto.
+ intros.
+ eapply modusponens.
+ simple eapply H.
+ (* error message with V8.3 :
+    Impossible to unify "?18" with "fun g : nat -> nat => ?6 = g". *)
+Abort.
+
+(* Regression test *)
+
+Definition fo : option nat -> nat := option_rec _ (fun a => 0) 0.
+
+(* This example revealed an incorrect evar restriction at some time
+   around October 2011 *)
+
+Goal forall (A:Type) (a:A) (P:forall A, A -> Prop), (P A a) /\ (P A a).
+intros.
+refine ((fun H => conj (proj1 H) (proj2 H)) _).
+Abort.
+
+(* The argument of e below failed to be inferred from r14219 (Oct 2011) to *)
+(* r14753 after the restrictions made on detecting Miller's pattern in the *)
+(* presence of alias, only the second-order unification procedure was *)
+(* able to solve this problem but it was deactivated for 8.4 in r14219 *)
+
+Definition k0
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, n = a) o :=
+ match o with (* note: match introduces an alias! *)
+ | Some a => e _ (j a)
+ | None => O
+ end.
+
+Definition k1
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j a).
+
+Definition k2
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b).
+
+(* Other examples about aliases involved in pattern unification *)
+
+Definition k3
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, let a' := a in n = a') a (b:=a) := e _ (j b).
+
+Definition k4
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, let a' := S a in n = a') a (b:=a) := e _ (j b).
+
+Definition k5
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, let a' := S a in exists n : nat, n = a') a (b:=a) := e _ (j b).
+
+Definition k6
+  (e:forall P : nat -> Prop, (exists n : nat, P n) -> nat)
+  (j : forall a, exists n : nat, let n' := S n in n' = a) a (b:=a) := e _ (j b).
+
+Definition k7
+  (e:forall P : nat -> Prop, (exists n : nat, let n' := n in P n') -> nat)
+  (j : forall a, exists n : nat, n = a) a (b:=a) := e _ (j b).
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 4fec6e7f..3f8a3bc4 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -342,7 +342,7 @@ case H1.
 exact H0.
 intros.
 exact n.
-Qed.
+Defined.
 Extraction oups.
 (*
 let oups h0 =
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index be4e0684..b25b502c 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -9,13 +9,12 @@ Inductive rBoolOp : Set :=
   | rAnd : rBoolOp
   | rEq : rBoolOp.
 
-Definition rlt (a b : rNat) : Prop :=
-  (a ?= b)%positive Datatypes.Eq = Datatypes.Lt.
+Definition rlt (a b : rNat) : Prop := Pcompare a b Eq = Lt.
 
 Definition rltDec : forall m n : rNat, {rlt m n} + {rlt n m \/ m = n}.
 intros n m; generalize (nat_of_P_lt_Lt_compare_morphism n m);
  generalize (nat_of_P_gt_Gt_compare_morphism n m);
- generalize (Pcompare_Eq_eq n m); case ((n ?= m)%positive Datatypes.Eq).
+ generalize (Pcompare_Eq_eq n m); case (Pcompare n m Eq).
 intros H' H'0 H'1; right; right; auto.
 intros H' H'0 H'1; left; unfold rlt in |- *.
 apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
diff --git a/test-suite/success/implicit.v b/test-suite/success/implicit.v
index ce3e692f..e8019a90 100644
--- a/test-suite/success/implicit.v
+++ b/test-suite/success/implicit.v
@@ -107,3 +107,20 @@ Context {A:Set}.
 Definition h (a:A) := a.
 End C.
 Check h 0.
+
+(* Check implicit arguments in arity of inductive types. The three
+   following examples used to fail before r13671 *)
+
+Inductive I {A} (a:A) : forall {n:nat}, Prop :=
+ | C : I a (n:=0).
+
+Inductive I2 (x:=0) : Prop :=
+ | C2 {p:nat} : p = 0 -> I2.
+Check C2 eq_refl.
+
+Inductive I3 {A} (x:=0) (a:A) : forall {n:nat}, Prop :=
+ | C3 : I3 a (n:=0).
+
+(* Check global implicit declaration over ref not in section *)
+
+Section D. Global Arguments eq [A] _ _. End D.
diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v
index 7626ecc4..234c4223 100644
--- a/test-suite/success/inds_type_sec.v
+++ b/test-suite/success/inds_type_sec.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index 3c8d8ea9..b24ed2f1 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -41,3 +41,26 @@ Proof.
   auto.
   auto.
 Qed.
+
+(* Check selection of occurrences by pattern *)
+
+Goal forall x, S x = S (S x).   
+intros.
+induction (S _) in |- * at -2.
+now_show (0=1).
+Undo 2.
+induction (S _) in |- * at 1 3.
+now_show (0=1).
+Undo 2.
+induction (S _) in |- * at 1.
+now_show (0=S (S x)).
+Undo 2.
+induction (S _) in |- * at 2.
+now_show (S x=0).
+Undo 2.
+induction (S _) in |- * at 3.
+now_show (S x=1).
+Undo 2.
+Fail induction (S _) in |- * at 4.
+Abort.
+
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.
diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v
index 41aa3b3e..fcadd150 100644
--- a/test-suite/success/mutual_ind.v
+++ b/test-suite/success/mutual_ind.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v
index 5a008f18..56cab0f6 100644
--- a/test-suite/success/polymorphism.v
+++ b/test-suite/success/polymorphism.v
@@ -9,4 +9,4 @@ End S.
 (*
 Check f nat nat : Set.
 *)
-Check I nat nat : Set.
+Check I nat nat : Set.
\ No newline at end of file
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
new file mode 100644
index 00000000..93a9ef11
--- /dev/null
+++ b/test-suite/success/proof_using.v
@@ -0,0 +1,61 @@
+Section Foo.
+
+Variable a : nat.
+
+Lemma l1 : True.
+Fail Proof using non_existing.
+Proof using a.
+exact I.
+Qed.
+
+Lemma l2 : True.
+Proof using a.
+Admitted.
+
+Lemma l3 : True.
+Proof using a.
+admit.
+Qed.
+
+End Foo.
+
+Check (l1 3).
+Check (l2 3).
+Check (l3 3).
+
+Section Bar.
+
+Variable T : Type.
+Variable a b : T.
+Variable H : a = b.
+
+Lemma l4 : a = b.
+Proof using H.
+exact H.
+Qed.
+
+End Bar.
+
+Check (l4 _ 1 1 _ : 1 = 1).
+
+Section S1.
+
+Variable v1 : nat.
+
+Section S2.
+
+Variable v2 : nat.
+
+Lemma deep : v1 = v2.
+Proof using v1 v2.
+admit.
+Qed.
+
+End S2.
+
+Check (deep 3 : v1 = 3).
+
+End S1.
+
+Check (deep 3 4 : 3 = 4).
+
diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
new file mode 100644
index 00000000..3241e133
--- /dev/null
+++ b/test-suite/success/remember.v
@@ -0,0 +1,8 @@
+(* Testing remember and co *)
+
+Lemma A : forall (P: forall X, X -> Prop), P nat 0 -> P nat 0.
+intros.
+Fail remember nat as X.
+Fail remember nat as X in H. (* This line used to succeed in 8.3 *)
+Fail remember nat as X in |- *.
+Abort.
diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v
index 3bce52fe..08c406be 100644
--- a/test-suite/success/rewrite.v
+++ b/test-suite/success/rewrite.v
@@ -108,3 +108,24 @@ intros.
 rewrite (H _).
 reflexivity.
 Qed.
+
+(* Example of rewriting of a degenerated pattern using the right-most
+   argument of the goal. This is sometimes used in contribs, even if
+   ad hoc. Here, we have the extra requirement that checking types
+   needs delta-conversion *)
+
+Axiom s : forall (A B : Type) (p : A * B), p = (fst p, snd p).
+Definition P := (nat * nat)%type.
+Goal forall x:P, x = x.
+intros. rewrite s.
+Abort.
+
+(* Test second-order unification and failure of pattern-unification *)
+
+Goal forall (P: forall Y, Y -> Prop) Y a, Y = nat -> (True -> P Y a) -> False.
+intros.
+(* The next line used to succeed between June and November 2011 *)
+(* causing ill-typed rewriting *)
+Fail rewrite H in H0.
+Abort.
+
diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v
new file mode 100644
index 00000000..d9ade314
--- /dev/null
+++ b/test-suite/success/searchabout.v
@@ -0,0 +1,60 @@
+
+(** Test of the different syntaxes of SearchAbout, in particular
+    with and without the [ ... ] delimiters *)
+
+SearchAbout plus.
+SearchAbout plus mult.
+SearchAbout "plus_n".
+SearchAbout plus "plus_n".
+SearchAbout "*".
+SearchAbout "*" "+".
+
+SearchAbout plus inside Peano.
+SearchAbout plus mult inside Peano.
+SearchAbout "plus_n" inside Peano.
+SearchAbout plus "plus_n" inside Peano.
+SearchAbout "*" inside Peano.
+SearchAbout "*" "+" inside Peano.
+
+SearchAbout plus outside Peano Logic.
+SearchAbout plus mult outside Peano Logic.
+SearchAbout "plus_n" outside Peano Logic.
+SearchAbout plus "plus_n" outside Peano Logic.
+SearchAbout "*" outside Peano Logic.
+SearchAbout "*" "+" outside Peano Logic.
+
+SearchAbout -"*" "+" outside Logic.
+SearchAbout -"*"%nat "+"%nat outside Logic.
+
+SearchAbout [plus].
+SearchAbout [plus mult].
+SearchAbout ["plus_n"].
+SearchAbout [plus "plus_n"].
+SearchAbout ["*"].
+SearchAbout ["*" "+"].
+
+SearchAbout [plus] inside Peano.
+SearchAbout [plus mult] inside Peano.
+SearchAbout ["plus_n"] inside Peano.
+SearchAbout [plus "plus_n"] inside Peano.
+SearchAbout ["*"] inside Peano.
+SearchAbout ["*" "+"] inside Peano.
+
+SearchAbout [plus] outside Peano Logic.
+SearchAbout [plus mult] outside Peano Logic.
+SearchAbout ["plus_n"] outside Peano Logic.
+SearchAbout [plus "plus_n"] outside Peano Logic.
+SearchAbout ["*"] outside Peano Logic.
+SearchAbout ["*" "+"] outside Peano Logic.
+
+SearchAbout [-"*" "+"] outside Logic.
+SearchAbout [-"*"%nat "+"%nat] outside Logic.
+
+
+(** The example in the Reference Manual *)
+
+Require Import ZArith.
+
+SearchAbout Zmult Zplus "distr".
+SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
+SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index 033b3f48..19693d70 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -130,3 +130,38 @@ intros f0 Q H.
 setoid_rewrite H.
 tauto.
 Qed.
+
+(** Check proper refreshing of the lemma application for multiple 
+   different instances in a single setoid rewrite. *)
+
+Section mult.
+  Context (fold : forall {A} {B}, (A -> B) -> A -> B).
+  Context (add : forall A, A -> A).
+  Context (fold_lemma : forall {A B f} {eqA : relation B} x, eqA (fold A B f (add A x)) (fold _ _ f x)).
+  Context (ab : forall B, A -> B).
+  Context (anat : forall A, nat -> A).
+
+Goal forall x, (fold _ _ (fun x => ab A x) (add A x) = anat _ (fold _ _ (ab nat) (add _ x))). 
+Proof. intros.
+  setoid_rewrite fold_lemma. 
+  change (fold A A (fun x0 : A => ab A x0) x = anat A (fold A nat (ab nat) x)).
+Abort.
+
+End mult.
+
+(** Current semantics for rewriting with typeclass constraints in the lemma 
+   does not fix the instance at the first unification, use [at], or simply rewrite for 
+   this semantics. *)
+
+Require Import Arith.
+
+Class Foo (A : Type) := {foo_neg : A -> A ; foo_prf : forall x : A, x = foo_neg x}.
+Instance: Foo nat. admit. Defined.
+Instance: Foo bool. admit. Defined.
+
+Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y.
+Proof. intros. setoid_rewrite <- foo_prf. change (beq_nat x 0 = y). Abort.
+
+Goal forall (x : nat) (y : bool), beq_nat (foo_neg x) 0 = foo_neg y.
+Proof. intros. setoid_rewrite <- @foo_prf at 1. change (beq_nat x 0 = foo_neg y). Abort.
+
diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v
new file mode 100644
index 00000000..d4191b93
--- /dev/null
+++ b/test-suite/success/simpl_tuning.v
@@ -0,0 +1,149 @@
+(* as it is dynamically inferred by simpl *)
+Arguments minus !n / m.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (match y with O => S x | S _ => _ end = 0) => idtac end.
+Abort. 
+
+(* we avoid exposing a match *)
+Arguments minus n m : simpl nomatch. 
+
+Lemma foo x : minus 0 x = 0.
+simpl.
+match goal with |- (0 = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+(* we unfold as soon as we have 1 args, but we avoid exposing a match *)
+Arguments minus n / m : simpl nomatch. 
+
+Lemma foo : minus 0 = fun x => 0.
+simpl.
+match goal with |- minus 0 = _ => idtac end.
+Abort.
+(* This does not work as one may expect. The point is that simpl is implemented
+   as "strong (whd_simpl_state)" and after unfolding minus you have
+   (fun m => match 0 => 0 | S n => ...) that is already in whd and exposes
+   a match, that of course "strong" would reduce away but at that stage
+   we don't know, and reducing by hand under the lambda is against whd *) 
+
+(* extra tuning for the usual heuristic *)
+Arguments minus !n / m : simpl nomatch. 
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+(* full control *)
+Arguments minus !n !m /.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+(* omitting /, that being immediately after the last ! is irrelevant *)
+Arguments minus !n !m.
+
+Lemma foo x y : S (S x) - S y = 0.
+simpl.
+match goal with |- (S x - y = 0) => idtac end.
+Abort.
+
+Lemma foo x y : S (S x) - (S (match y with O => O | S z => S z end)) = 0.
+simpl.
+match goal with |-(S x - (match y with O => _ | S _ => _ end) = 0) => idtac end.
+Abort.
+
+Definition pf (D1 C1 : Type) (f : D1 -> C1) (D2 C2 : Type) (g : D2 -> C2) := 
+  fun x => (f (fst x), g (snd x)).
+
+Delimit Scope foo_scope with F.
+Notation "@@" := nat (only parsing) : foo_scope.
+Notation "@@" := (fun x => x) (only parsing).
+
+Arguments pf {D1%F C1%type} f [D2 C2] g x : simpl never.
+
+Lemma foo x : @pf @@ nat @@ nat nat @@ x = pf @@ @@ x.
+Abort.
+
+Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x).
+
+(* fcomp is unfolded if applied to 6 args *)
+Arguments fcomp {A B C}%type f g x /.
+
+Notation "f \o g" := (fcomp f g) (at level 50).
+
+Lemma foo (f g h : nat -> nat) x : pf (f \o g) h x = pf f h (g (fst x), snd x).
+simpl.
+match goal with |- (pf (f \o g) h x = _) => idtac end.
+case x; intros x1 x2. 
+simpl.
+match goal with |- (pf (f \o g) h _ = pf f h _) => idtac end.
+unfold pf; simpl.
+match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end.
+Abort. 
+
+Definition volatile := fun x : nat => x.
+Arguments volatile /.
+
+Lemma foo : volatile = volatile.
+simpl.
+match goal with |- (fun _ => _) = _ => idtac end.
+Abort.
+
+Set Implicit Arguments.
+
+Section S1.
+
+Variable T1 : Type.
+
+Section S2.
+
+Variable T2 : Type.
+
+Fixpoint f (x : T1) (y : T2) n (v : unit) m {struct n} : nat :=
+  match n, m with
+  | 0,_ => 0
+  | S _, 0 => n
+  | S n', S m' => f x y n' v m' end.
+
+Global Arguments f x y !n !v !m.
+
+Lemma foo x y n m : f x y (S n) tt m = f x y (S n) tt (S m).
+simpl.
+match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end.
+Abort.
+
+End S2.
+
+Lemma foo T x y n m : @f T x y (S n) tt m = @f T x y (S n) tt (S m).
+simpl.
+match goal with |- (f _ _ _ _ _ = f _ _ _ _ _) => idtac end.
+Abort.
+
+End S1.
+
+Arguments f : clear implicits and scopes.
+
diff --git a/test-suite/success/telescope_canonical.v b/test-suite/success/telescope_canonical.v
new file mode 100644
index 00000000..8a607c93
--- /dev/null
+++ b/test-suite/success/telescope_canonical.v
@@ -0,0 +1,12 @@
+Structure Inner := mkI { is :> Type }.
+Structure Outer := mkO { os :> Inner }.
+
+Canonical Structure natInner := mkI nat.
+Canonical Structure natOuter := mkO natInner.
+
+Definition hidden_nat := nat.
+
+Axiom P : forall S : Outer, is (os S) -> Prop.
+
+Lemma foo (n : hidden_nat) : P _ n.
+Admitted.
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 66c4e080..5649e2f7 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index ddf122e8..997dceb4 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -21,6 +21,12 @@ Proof.
 intros; apply H.
 Qed.
 
+  (* Feature introduced June 2011 *)
+
+Lemma l7 : forall x (P:nat->Prop), (forall f, P (f x)) -> P (x+x).
+Proof.
+intros x P H; apply H.
+Qed.
 
 (* Example submitted for Zenon *)
 
@@ -90,12 +96,14 @@ intros.
 apply H.
 Qed.
 
+(* Feature deactivated in commit 14189 (see commit log)
 (* Test instanciation of evars by unification *)
 
 Goal (forall x, 0 + x = 0 -> True) -> True.
 intros; eapply H.
 rewrite <- plus_n_Sm. (* should refine ?x with S ?x' *)
 Abort.
+*)
 
 (* Check handling of identity equation between evars *)
 (* The example failed to pass until revision 10623 *)
@@ -135,4 +143,44 @@ Goal (forall (A B : Set) (f : A -> B), (fun x => f x) = f) ->
  forall (A B C : Set) (g : (A -> B) -> C) (f : A -> B), g (fun x => f x) = g f.
 Proof.
   intros.
-  rewrite H.
+  rewrite H with (f:=f0).
+Abort.
+
+(* Three tests provided by Dan Grayson as part of a custom patch he
+   made for a more powerful "destruct" for handling Voevodsky's
+   Univalent Foundations. The test checks if second-order matching in
+   tactic unification is able to guess by itself on which dependent
+   terms to abstract so that the elimination predicate is well-typed *)
+
+Definition test1 (X : Type) (x : X) (fxe : forall x1 : X, identity x1 x1) :
+  identity (fxe x) (fxe x).
+Proof. destruct (fxe x). apply identity_refl. Defined.
+
+(* a harder example *)
+
+Definition UU := Type .
+Inductive paths {T:Type}(t:T): T -> UU := idpath: paths t t.
+Inductive foo (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU := newfoo : foo x0 x0.
+Definition idonfoo {X0:UU} {x0:X0} {X1:UU} {x1:X1} : foo x0 x1 -> foo x0 x1.
+Proof. intros t. exact t. Defined.
+
+Lemma test2 (T:UU) (t:T) (k : foo t t) : paths k (idonfoo k).
+Proof.
+  destruct k.
+  apply idpath.
+Defined.
+
+(* an example with two constructors *)
+
+Inductive foo' (X0:UU) (x0:X0) : forall (X:UU)(x:X), UU :=
+| newfoo1 : foo' x0 x0
+| newfoo2 : foo' x0 x0 .
+Definition idonfoo' {X0:UU} {x0:X0} {X1:UU} {x1:X1} :
+  foo' x0 x1 -> foo' x0 x1.
+Proof. intros t. exact t. Defined.
+Lemma test3 (T:UU) (t:T) (k : foo' t t) : paths k (idonfoo' k).
+Proof.
+  destruct k.
+  apply idpath.
+  apply idpath.
+Defined.
diff --git a/test-suite/success/universes-coercion.v b/test-suite/success/universes-coercion.v
new file mode 100644
index 00000000..d7504340
--- /dev/null
+++ b/test-suite/success/universes-coercion.v
@@ -0,0 +1,22 @@
+(* This example used to emphasize the absence of LEGO-style universe
+   polymorphism; Matthieu's improvements of typing on 2011/3/11 now
+   makes (apparently) that Amokrane's automatic eta-expansion in the
+   coercion mechanism works; this makes its illustration as a "weakness"
+   of universe polymorphism obsolete (example submitted by Randy Pollack).
+
+   Note that this example is not an evidence that the current
+   non-kernel eta-expansion behavior is the most expected one.  
+*)
+
+Parameter K : forall T : Type, T -> T.
+Check (K (forall T : Type, T -> T) K).
+
+(*
+   note that the inferred term is
+     "(K (forall T (* u1 *) : Type, T -> T) (fun T:Type (* u1 *) => K T))"
+   which is not eta-equivalent to 
+     "(K (forall T : Type, T -> T) K"
+   because the eta-expansion of the latter
+     "(K (forall T : Type, T -> T) (fun T:Type (* u2 *) => K T)"
+  assuming K of type "forall T (* u2 *) : Type, T -> T"
+*)