Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg

41 files changed, 1449 insertions, 44 deletions

diff --git a/test-suite/bugs/closed/shouldfail/1898.v b/test-suite/bugs/closed/shouldfail/1898.v
new file mode 100644
index 00000000..92490eb9
--- /dev/null
+++ b/test-suite/bugs/closed/shouldfail/1898.v
@@ -0,0 +1,5 @@
+(* folding should not allow circular dependencies *)
+
+Lemma bug_fold_unfold : True.
+  set (h := 1).
+  fold h in h.
diff --git a/test-suite/bugs/closed/shouldsucceed/121.v b/test-suite/bugs/closed/shouldsucceed/121.v
index d193aa73..8c5a3885 100644
--- a/test-suite/bugs/closed/shouldsucceed/121.v
+++ b/test-suite/bugs/closed/shouldsucceed/121.v
@@ -4,7 +4,7 @@ Section Setoid_Bug.
 
 Variable X:Type -> Type.
 Variable Xeq : forall A, (X A) -> (X A) -> Prop.
-Hypothesis Xst : forall A, Equivalence (X A) (Xeq A).
+Hypothesis Xst : forall A, Equivalence (Xeq A).
 
 Variable map : forall A B, (A -> B) -> X A -> X B.
 
diff --git a/test-suite/bugs/closed/shouldsucceed/1791.v b/test-suite/bugs/closed/shouldsucceed/1791.v
new file mode 100644
index 00000000..694f056e
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1791.v
@@ -0,0 +1,38 @@
+(* simpl performs eta expansion *)
+
+Set Implicit Arguments.
+Require Import List.
+
+Definition k0 := Set.
+Definition k1 := k0 -> k0.
+
+(** iterating X n times *)
+Fixpoint Pow (X:k1)(k:nat){struct k}:k1:=
+  match k with 0 => fun X => X
+             |  S k' => fun A => X (Pow X k' A)   
+  end.
+
+Parameter Bush: k1.
+Parameter BushToList: forall (A:k0), Bush A ->  list A.
+
+Definition BushnToList (n:nat)(A:k0)(t:Pow Bush n A): list A.
+Proof.
+  intros.
+  induction n.
+  exact (t::nil).
+  simpl in t.
+  exact (flat_map IHn (BushToList t)).
+Defined.
+
+Parameter bnil : forall (A:k0), Bush A.
+Axiom BushToList_bnil: forall (A:k0), BushToList (bnil A) = nil(A:=A).
+
+Lemma BushnToList_bnil (n:nat)(A:k0):
+  BushnToList (S n) A (bnil (Pow Bush n A)) = nil.
+Proof.
+  intros.
+  simpl.
+  rewrite BushToList_bnil.
+  simpl.
+  reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1891.v b/test-suite/bugs/closed/shouldsucceed/1891.v
new file mode 100644
index 00000000..11124cdd
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1891.v
@@ -0,0 +1,13 @@
+(* Check evar-evar unification *)
+ Inductive T (A: Set): Set := mkT: unit -> T A.
+
+  Definition f (A: Set) (l: T A): unit := tt.
+
+  Implicit Arguments f [A].
+
+  Lemma L (x: T unit): (unit -> T unit) -> unit.
+  Proof.
+    refine (fun x => match x return _ with mkT n => fun g => f (g _) end).
+    trivial.
+  Qed.
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1900.v b/test-suite/bugs/closed/shouldsucceed/1900.v
new file mode 100644
index 00000000..cf03efda
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1900.v
@@ -0,0 +1,8 @@
+Parameter A : Type .
+
+Definition eq_A := @eq A.
+
+Goal forall x, eq_A x x.
+intros.
+reflexivity.
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1901.v b/test-suite/bugs/closed/shouldsucceed/1901.v
new file mode 100644
index 00000000..598db366
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1901.v
@@ -0,0 +1,11 @@
+Require Import Relations.
+
+Record Poset{A:Type}(Le : relation A) : Type :=
+  Build_Poset
+  { 
+    Le_refl : forall x : A, Le x x; 
+    Le_trans : forall x y z : A, Le x y -> Le y z -> Le x z; 
+    Le_antisym : forall x y : A, Le x y -> Le y x -> x = y }.
+
+Definition nat_Poset : Poset Peano.le.
+Admitted.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1907.v b/test-suite/bugs/closed/shouldsucceed/1907.v
new file mode 100644
index 00000000..55fc8231
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1907.v
@@ -0,0 +1,7 @@
+(* An example of type inference *)
+
+Axiom A : Type.
+Definition f (x y : A) := x.
+Axiom g : forall x y : A, f x y = y -> Prop.
+Axiom x : A.
+Check (g x _ (refl_equal x)).
diff --git a/test-suite/bugs/closed/shouldsucceed/1918.v b/test-suite/bugs/closed/shouldsucceed/1918.v
new file mode 100644
index 00000000..9d4a3e04
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1918.v
@@ -0,0 +1,377 @@
+(** Occur-check for Meta (up to delta) *)
+
+(** LNMItPredShort.v Version 2.0 July 2008 *)
+(** does not need impredicative Set, runs under V8.2, tested with SVN 11296 *)
+
+(** Copyright Ralph Matthes, I.R.I.T.,  C.N.R.S. & University of Toulouse*)
+
+
+Set Implicit Arguments.
+
+(** the universe of all monotypes *)
+Definition k0 := Set.
+
+(** the type of all type transformations *)
+Definition k1 := k0 -> k0.
+
+(** the type of all rank-2 type transformations *)
+Definition k2 := k1 -> k1.
+
+(** polymorphic identity *)
+Definition id : forall (A:Set), A -> A := fun A x => x.
+
+(** composition *)
+Definition comp (A B C:Set)(g:B->C)(f:A->B) : A->C := fun x => g (f x).
+
+Infix "o" := comp (at level 90).
+
+Definition sub_k1 (X Y:k1) : Type :=
+     forall A:Set, X A -> Y A.
+
+Infix "c_k1" := sub_k1 (at level 60).
+
+(** monotonicity *)
+Definition mon (X:k1) : Type := forall (A B:Set), (A -> B) -> X A -> X B.
+
+(** extensionality *)
+Definition ext (X:k1)(h: mon X): Prop :=
+  forall (A B:Set)(f g:A -> B), 
+        (forall a, f a = g a) -> forall r, h _ _ f r = h _ _ g r.
+
+(** first functor law *)
+Definition fct1 (X:k1)(m: mon X) : Prop :=
+  forall (A:Set)(x:X A), m _ _ (id(A:=A)) x = x.
+
+(** second functor law *)
+Definition fct2 (X:k1)(m: mon X) : Prop :=
+ forall (A B C:Set)(f:A -> B)(g:B -> C)(x:X A), 
+       m _ _ (g o f) x = m _ _ g (m _ _ f x).
+
+(** pack up the good properties of the approximation into
+  the notion of an extensional functor *)
+Record EFct (X:k1) : Type := mkEFct
+  { m : mon X;
+     e : ext m;
+     f1 : fct1 m;
+     f2 : fct2 m }.
+
+(** preservation of extensional functors *)
+Definition pEFct (F:k2) : Type :=
+  forall (X:k1), EFct X -> EFct (F X).
+
+
+(** we show some closure properties of pEFct, depending on such properties 
+      for EFct *)
+
+Definition moncomp (X Y:k1)(mX:mon X)(mY:mon Y): mon (fun A => X(Y A)).
+Proof.
+  red.
+  intros X Y mX mY A B f x.
+  exact (mX (Y A)(Y B) (mY A B f) x).
+Defined.
+
+(** closure under composition *)
+Lemma compEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X(Y A)).
+Proof.
+  intros X Y ef1 ef2.
+  apply (mkEFct(m:=moncomp (m ef1) (m ef2))); red; intros; unfold moncomp.
+(* prove ext *)
+  apply (e ef1).
+  intro.
+  apply (e ef2); trivial.
+(* prove fct1 *)
+  rewrite (e ef1 (m ef2 (id (A:=A))) (id(A:=Y A))).
+  apply (f1 ef1).
+  intro.
+  apply (f1 ef2).
+(* prove fct2 *)
+  rewrite (e ef1 (m ef2 (g o f))((m ef2 g)o(m ef2 f))).
+  apply (f2 ef1).
+  intro.
+  unfold comp at 2.
+  apply (f2 ef2).
+Defined.
+
+Corollary comppEFct (F G:k2): pEFct F -> pEFct G -> 
+      pEFct (fun X A => F X (G X A)).
+Proof.
+  red.
+  intros.
+  apply compEFct; auto.
+Defined.
+
+(** closure under sums *)
+Lemma sumEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A + Y A)%type.
+Proof.
+  intros X Y ef1 ef2.
+  set (m12:=fun (A B:Set)(f:A->B) x => match x with 
+    | inl y => inl _ (m ef1 f y)
+    | inr y => inr _ (m ef2 f y)
+  end).
+  apply (mkEFct(m:=m12)); red; intros.
+(* prove ext *)
+  destruct r.
+  simpl.
+  apply (f_equal (fun x=>inl (A:=X B) (Y B) x)).
+  apply (e ef1); trivial.
+  simpl.
+  apply (f_equal (fun x=>inr (X B) (B:=Y B) x)).
+  apply (e ef2); trivial.
+(* prove fct1 *)
+  destruct x.
+  simpl.
+  apply (f_equal (fun x=>inl (A:=X A) (Y A) x)).
+  apply (f1 ef1).
+  simpl.
+  apply (f_equal (fun x=>inr (X A) (B:=Y A) x)).
+  apply (f1 ef2).
+(* prove fct2 *)
+  destruct x.
+  simpl.
+  rewrite (f2 ef1); reflexivity.
+  simpl.
+  rewrite (f2 ef2); reflexivity.
+Defined.
+
+Corollary sumpEFct (F G:k2): pEFct F -> pEFct G -> 
+      pEFct (fun X A => F X A + G X A)%type.
+Proof.
+  red.
+  intros.
+  apply sumEFct; auto.
+Defined.
+
+(** closure under products *)
+Lemma prodEFct (X Y:k1): EFct X -> EFct Y -> EFct (fun A => X A * Y A)%type.
+Proof.
+  intros X Y ef1 ef2.
+  set (m12:=fun (A B:Set)(f:A->B) x => match x with 
+    (x1,x2) => (m ef1 f x1, m ef2 f x2) end).
+  apply (mkEFct(m:=m12)); red; intros.
+(* prove ext *)
+  destruct r as [x1 x2].
+  simpl.
+  apply injective_projections; simpl.
+  apply (e ef1); trivial.
+  apply (e ef2); trivial.
+(* prove fct1 *)
+  destruct x as [x1 x2].
+  simpl.
+  apply injective_projections; simpl.
+  apply (f1 ef1).
+  apply (f1 ef2).
+(* prove fct2 *)
+  destruct x as [x1 x2].
+  simpl.
+  apply injective_projections; simpl.
+  apply (f2 ef1).
+  apply (f2 ef2).
+Defined.
+
+Corollary prodpEFct (F G:k2): pEFct F -> pEFct G -> 
+      pEFct (fun X A => F X A * G X A)%type.
+Proof.
+  red.
+  intros.
+  apply prodEFct; auto.
+Defined.
+
+(** the identity in k2 preserves extensional functors *)
+Lemma idpEFct: pEFct (fun X => X).
+Proof.
+  red.
+  intros.
+  assumption.
+Defined.
+
+(** a variant for the eta-expanded identity *)
+Lemma idpEFct_eta: pEFct (fun X A => X A).
+Proof.
+  red.
+  intros X ef.
+  destruct ef as [m0 e0 f01 f02].
+  change (mon X) with (mon (fun A => X A)) in m0.
+  apply (mkEFct (m:=m0) e0 f01 f02).
+Defined.
+
+(** the identity in k1 "is" an extensional functor *)
+Lemma idEFct: EFct (fun A => A).
+Proof.
+  set (mId:=fun A B (f:A->B)(x:A) => f x).
+  apply (mkEFct(m:=mId)).
+  red.
+  intros.
+  unfold mId.
+  apply H.
+  red.
+  reflexivity.
+  red.
+  reflexivity.
+Defined.
+
+(** constants in k2 *)
+Lemma constpEFct (X:k1): EFct X  -> pEFct (fun _ => X).
+Proof.
+  red.
+  intros.
+  assumption.
+Defined.
+
+(** constants in k1 *)
+Lemma constEFct (C:Set): EFct (fun _ => C).
+Proof.
+  intro.
+  set (mC:=fun A B (f:A->B)(x:C) => x).
+  apply (mkEFct(m:=mC)); red; intros; unfold mC; reflexivity.
+Defined.
+
+
+(** the option type *)
+Lemma optionEFct: EFct (fun (A:Set) => option A).
+  apply (mkEFct (X:=fun (A:Set) => option A)(m:=option_map)); red; intros.
+  destruct r.
+  simpl.
+  rewrite H.
+  reflexivity.
+  reflexivity.
+  destruct x; reflexivity.
+  destruct x; reflexivity.
+Defined.
+
+
+(** natural transformations from (X,mX) to (Y,mY) *)
+Definition NAT(X Y:k1)(j:X c_k1 Y)(mX:mon X)(mY:mon Y) : Prop :=
+  forall (A B:Set)(f:A->B)(t:X A), j B (mX A B f t) = mY _ _ f (j A t).
+
+
+Module Type LNMIt_Type.
+
+Parameter F:k2.
+Parameter FpEFct: pEFct F.
+Parameter mu20: k1. 
+Definition  mu2: k1:= fun A => mu20 A.
+Parameter mapmu2: mon mu2.
+Definition MItType: Type :=
+  forall G : k1, (forall X : k1, X c_k1 G -> F X c_k1 G) -> mu2 c_k1 G.
+Parameter MIt0 : MItType.
+Definition MIt : MItType:= fun G s A t => MIt0 s t. 
+Definition InType : Type := 
+    forall (X:k1)(ef:EFct X)(j: X c_k1 mu2), 
+        NAT j (m ef) mapmu2 -> F X c_k1 mu2.
+Parameter In : InType.
+Axiom mapmu2Red : forall (A:Set)(X:k1)(ef:EFct X)(j: X c_k1 mu2)
+    (n: NAT j (m ef) mapmu2)(t: F X A)(B:Set)(f:A->B), 
+            mapmu2 f (In ef n t) = In ef n (m (FpEFct ef) f t).
+Axiom MItRed : forall (G : k1)
+  (s : forall X : k1, X c_k1 G -> F X c_k1 G)(X : k1)(ef:EFct X)(j: X c_k1 mu2)
+      (n: NAT j (m ef) mapmu2)(A:Set)(t:F X A),
+     MIt s (In ef n t) = s X (fun A => (MIt s (A:=A)) o (j A)) A t.
+Definition mu2IndType : Prop :=
+  forall (P : (forall A : Set, mu2 A -> Prop)),
+       (forall (X : k1)(ef:EFct X)(j : X c_k1 mu2)(n: NAT j (m ef) mapmu2),
+          (forall (A : Set) (x : X A), P A (j A x)) ->
+        forall (A:Set)(t : F X A), P A (In ef n t)) ->
+    forall (A : Set) (r : mu2 A), P A r.
+Axiom mu2Ind : mu2IndType.
+
+End LNMIt_Type.
+
+(** BushDepPredShort.v Version 0.2 July 2008 *)
+(** does not need impredicative Set, produces stack overflow under V8.2, tested
+with SVN 11296 *)
+
+(** Copyright  Ralph Matthes, I.R.I.T.,  C.N.R.S. & University of Toulouse *)
+
+Set Implicit Arguments.
+
+Require Import List.
+
+Definition listk1 (A:Set) : Set := list A.
+Open Scope type_scope.
+
+Definition BushF(X:k1)(A:Set) :=  unit + A  * X (X A).
+
+Definition bushpEFct : pEFct BushF.
+Proof.
+  unfold BushF.
+  apply sumpEFct.
+  apply constpEFct.
+  apply constEFct.
+  apply prodpEFct.
+  apply constpEFct.
+  apply idEFct.
+  apply comppEFct.
+  apply idpEFct.
+  apply idpEFct_eta.
+Defined.
+
+Module Type BUSH := LNMIt_Type with Definition F:=BushF
+                                                with Definition FpEFct :=
+bushpEFct.
+
+Module Bush (BushBase:BUSH).
+
+Definition Bush : k1 := BushBase.mu2.
+
+Definition bush : mon Bush := BushBase.mapmu2.
+
+End Bush.
+
+
+Definition Id : k1 := fun X => X.
+
+Fixpoint Pow (X:k1)(k:nat){struct k}:k1:=
+  match k with 0 => Id
+             |  S k' => fun A => X (Pow X k' A)
+  end.
+
+Fixpoint POW  (k:nat)(X:k1)(m:mon X){struct k} : mon (Pow X k) :=
+  match k return mon (Pow X k)
+      with 0 => fun _ _ f  => f 
+     |  S k' => fun _ _ f  => m _ _ (POW k' m f) 
+   end.
+
+Module Type BushkToList_Type.
+
+Declare Module Import BP: BUSH.
+Definition F:=BushF.
+Definition FpEFct:= bushpEFct.
+Definition mu20 := mu20.
+Definition mu2 := mu2.
+Definition mapmu2 := mapmu2.
+Definition MItType:= MItType.
+Definition MIt0 := MIt0.
+Definition MIt := MIt.
+Definition InType := InType.
+Definition In := In.
+Definition mapmu2Red:=mapmu2Red.
+Definition MItRed:=MItRed.
+Definition mu2IndType:=mu2IndType.
+Definition mu2Ind:=mu2Ind.
+
+Definition  Bush:= mu2.
+Module BushM := Bush BP.
+
+Parameter BushkToList: forall(k:nat)(A:k0)(t:Pow Bush k A), list A.
+Axiom BushkToList0: forall(A:k0)(t:Pow Bush 0 A), BushkToList 0 A t = t::nil.
+
+End BushkToList_Type.
+
+Module BushDep (BushkToListM:BushkToList_Type).
+
+Module Bush := Bush BushkToListM.
+
+Import Bush.
+Import BushkToListM.
+
+
+Lemma BushkToList0NAT: NAT(Y:=listk1) (BushkToList 0) (POW 0 bush) map.
+Proof.
+  red.
+  intros.
+  simpl.
+  rewrite BushkToList0.
+(* stack overflow for coqc and coqtop *)
+
+
+Abort.
diff --git a/test-suite/bugs/closed/shouldsucceed/1925.v b/test-suite/bugs/closed/shouldsucceed/1925.v
new file mode 100644
index 00000000..17eb721a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1925.v
@@ -0,0 +1,22 @@
+(* Check that the analysis of projectable rel's in an evar instance is up to
+   aliases *)
+
+Require Import List.
+
+Definition compose (A B C : Type) (g : B -> C) (f : A -> B) : A -> C := 
+  fun x : A => g(f x).
+
+Definition map_fuse' : 
+  forall (A B C : Type) (g : B -> C) (f : A -> B) (xs : list A), 
+    (map g (map f xs)) = map (compose _ _ _ g f) xs 
+    :=
+    fun A B C g f => 
+      (fix loop (ys : list A) {struct ys} :=
+        match ys as ys return (map g (map f ys)) = map (compose _ _ _ g f) ys
+        with
+        | nil => refl_equal nil
+        | x :: xs =>
+           match loop xs in eq _ a return eq _  ((g (f x)) :: a) with
+            | refl_equal => refl_equal (map g (map f (x :: xs)))
+           end
+        end).
diff --git a/test-suite/bugs/closed/shouldsucceed/1931.v b/test-suite/bugs/closed/shouldsucceed/1931.v
new file mode 100644
index 00000000..bc8be78f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1931.v
@@ -0,0 +1,29 @@
+
+
+Set Implicit Arguments.
+
+Inductive T (A:Set) : Set :=
+ app : T A -> T A -> T A.
+
+Fixpoint map (A B:Set)(f:A->B)(t:T A) : T B :=
+ match t with
+   app t1 t2 => app (map f t1)(map f t2)
+ end. 
+
+Fixpoint subst (A B:Set)(f:A -> T B)(t:T A) :T B :=
+ match t with
+    app t1 t2 => app (subst f t1)(subst f t2)
+ end.
+
+(* This is the culprit: *)
+Definition k0:=Set.
+
+(** interaction of subst with map *)
+Lemma substLaw1 (A:k0)(B C:Set)(f: A -> B)(g:B -> T C)(t: T A): 
+ subst g (map f t) = subst (fun x => g (f x)) t.
+Proof.
+ intros.
+ generalize B C f g; clear B C f g.
+ induction t; intros; simpl.
+ f_equal.
+Admitted.
diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v
new file mode 100644
index 00000000..641dcb7a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1935.v
@@ -0,0 +1,21 @@
+Definition f  (n:nat) := n = n.
+
+Lemma f_refl : forall n , f n.
+intros. reflexivity. 
+Qed.
+
+Definition f'  (x:nat) (n:nat) := n = n.
+
+Lemma f_refl' : forall n , f' n n.
+Proof.
+ intros. reflexivity. 
+Qed.
+
+Require Import ZArith.
+
+Definition f'' (a:bool) := if a then eq (A:= Z) else Zlt.
+
+Lemma f_refl'' : forall n , f'' true n n.
+Proof.
+ intro. reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1963.v b/test-suite/bugs/closed/shouldsucceed/1963.v
new file mode 100644
index 00000000..11e2ee44
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1963.v
@@ -0,0 +1,19 @@
+(* Check that "dependent inversion" behaves correctly w.r.t to universes *)
+
+Require Import Eqdep.
+
+Set Implicit Arguments.
+
+Inductive illist(A:Type) : nat -> Type :=
+  illistn : illist A 0
+| illistc : forall n:nat, A -> illist A n -> illist A (S n).
+
+Inductive isig (A:Type)(P:A -> Type) : Type :=
+  iexists : forall x : A, P x -> isig P.
+
+Lemma inv : forall (A:Type)(n n':nat)(ts':illist A n'), n' = S n ->
+  isig (fun t => isig (fun ts =>
+    eq_dep nat (fun n => illist A n) n' ts' (S n) (illistc t ts))).
+Proof.
+intros.
+dependent inversion ts'.
diff --git a/test-suite/bugs/closed/shouldsucceed/1977.v b/test-suite/bugs/closed/shouldsucceed/1977.v
new file mode 100644
index 00000000..28715040
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1977.v
@@ -0,0 +1,4 @@
+Inductive T {A} : Prop := c : A -> T.
+Goal (@T nat).
+apply c. exact 0.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1981.v b/test-suite/bugs/closed/shouldsucceed/1981.v
new file mode 100644
index 00000000..0c3b96da
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1981.v
@@ -0,0 +1,5 @@
+Implicit Arguments ex_intro [A].
+
+Goal exists n : nat, True.
+  eapply ex_intro. exact 0. exact I. 
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2001.v b/test-suite/bugs/closed/shouldsucceed/2001.v
new file mode 100644
index 00000000..323021de
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2001.v
@@ -0,0 +1,20 @@
+(* Automatic computing of guard in "Theorem with"; check that guard is not
+   computed when the user explicitly indicated it *)
+
+Inductive T : Set :=
+| v : T. 
+
+Definition f (s:nat) (t:T) : nat.
+fix 2.
+intros s t.
+refine
+  match t with
+  | v => s
+  end.
+Defined.
+           
+Lemma test :
+  forall s, f s v = s.
+Proof.    
+reflexivity.
+Qed.        
diff --git a/test-suite/bugs/closed/shouldsucceed/2017.v b/test-suite/bugs/closed/shouldsucceed/2017.v
new file mode 100644
index 00000000..948cea3e
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2017.v
@@ -0,0 +1,15 @@
+(* Some check of Miller's pattern inference - used to fail in 8.2 due
+   first to the presence of aliases, secondly due to the absence of
+   restriction of the potential interesting variables to the subset of
+   variables effectively occurring in the term to instantiate *)
+
+Set Implicit Arguments.
+
+Variable choose : forall(P : bool -> Prop)(H : exists x, P x), bool.
+
+Variable H : exists x : bool, True.
+ 
+Definition coef :=
+match Some true	with
+  Some _ => @choose _ H |_ => true 
+end .      
diff --git a/test-suite/bugs/closed/shouldsucceed/2021.v b/test-suite/bugs/closed/shouldsucceed/2021.v
new file mode 100644
index 00000000..e598e5ae
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2021.v
@@ -0,0 +1,23 @@
+(* correct failure of injection/discriminate on types whose inductive
+   status derives from the substitution of an argument *)
+
+Inductive t : nat -> Type :=
+| M : forall n: nat, nat -> t n.
+
+Lemma eq_t : forall n n' m m',
+   existT (fun B : Type => B) (t n) (M n m) =
+   existT (fun B : Type => B) (t n') (M n' m') -> True.
+Proof.
+  intros.
+  injection H.
+  intro Ht.
+  exact I.
+Qed.
+
+Lemma eq_t' : forall n n' : nat,
+   existT (fun B : Type => B) (t n) (M n 0) =
+   existT (fun B : Type => B) (t n') (M n' 1) -> True.
+Proof.
+  intros.
+  discriminate H || exact I.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2027.v b/test-suite/bugs/closed/shouldsucceed/2027.v
new file mode 100644
index 00000000..fb53c6ef
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2027.v
@@ -0,0 +1,11 @@
+
+Parameter T : Type -> Type.
+Parameter f : forall {A}, T A -> T A.
+Parameter P : forall {A}, T A -> Prop.
+Axiom f_id : forall {A} (l : T A), f l = l.
+
+Goal forall A (p : T A), P p.
+Proof.
+  intros.
+  rewrite <- f_id.
+Admitted.
\ No newline at end of file
diff --git a/test-suite/check b/test-suite/check
index 47960e98..bed86c41 100755
--- a/test-suite/check
+++ b/test-suite/check
@@ -3,9 +3,9 @@
 # Automatic test of Coq
 
 if [ "$1" = -byte ]; then
-  coqtop="../bin/coqtop.byte -q -batch"
+  coqtop="../bin/coqtop.byte -boot -q -batch"
 else
-  coqtop="../bin/coqtop -q -batch"
+  coqtop="../bin/coqtop -boot -q -batch"
 fi
 
 command="$coqtop -top Top -load-vernac-source"
diff --git a/test-suite/complexity/autodecomp.v b/test-suite/complexity/autodecomp.v
new file mode 100644
index 00000000..8916b104
--- /dev/null
+++ b/test-suite/complexity/autodecomp.v
@@ -0,0 +1,11 @@
+(* This example used to be in (at least) exponential time in the number of
+   conjunctive types in the hypotheses before revision 11713 *)
+(* Expected time < 1.50s *)
+
+Goal
+True/\True->
+True/\True->
+True/\True->
+False/\False.
+
+Time auto decomp.
diff --git a/test-suite/failure/Reordering.v b/test-suite/failure/Reordering.v
new file mode 100644
index 00000000..7b36d1c3
--- /dev/null
+++ b/test-suite/failure/Reordering.v
@@ -0,0 +1,5 @@
+(* Testing that hypothesis order (following a conversion/folding) is checked *)
+
+Goal forall (A:Set) (x:A) (A':=A), True.
+intros.
+change ((fun (_:A') => Set) x) in (type of A).
diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v
index 46208c29..7e07a905 100644
--- a/test-suite/failure/guard.v
+++ b/test-suite/failure/guard.v
@@ -8,3 +8,14 @@
 
 Fixpoint F (n:nat) : False := F (match F n with end).
 
+(* de Bruijn mix-up *)
+(* If accepted, Eval compute in f 0. loops *)
+Definition f :=
+  let f (f1 f2:nat->nat) := f1 in
+  let _ := 0 in
+  let _ := 0 in
+  let g (f1 f2:nat->nat) := f2 in
+  let h := f in (* h = Rel 4 *)
+  fix F (n:nat) : nat :=
+  h F S n. (* here Rel 4 = g *)
+  
diff --git a/test-suite/output/ArgumentsScope.v b/test-suite/output/ArgumentsScope.v
index 13b5e13d..1ff53294 100644
--- a/test-suite/output/ArgumentsScope.v
+++ b/test-suite/output/ArgumentsScope.v
@@ -1,4 +1,4 @@
-(* A few tests to check Argument Scope Global command *)
+(* A few tests to check Global Argument Scope command *)
 
 Section A.
 Variable a : bool -> bool.
@@ -11,11 +11,11 @@ About b.
 About negb''.
 About negb'.
 About negb.
-Arguments Scope Global negb'' [ _ ].
-Arguments Scope Global negb' [ _ ].
-Arguments Scope Global negb [ _ ].
-Arguments Scope Global a [ _ ].
-Arguments Scope Global b [ _ ].
+Global Arguments Scope negb'' [ _ ].
+Global Arguments Scope negb' [ _ ].
+Global Arguments Scope negb [ _ ].
+Global Arguments Scope a [ _ ].
+Global Arguments Scope b [ _ ].
 About a.
 About b.
 About negb.
diff --git a/test-suite/output/Cases.out b/test-suite/output/Cases.out
index 995754a6..1f0e12d3 100644
--- a/test-suite/output/Cases.out
+++ b/test-suite/output/Cases.out
@@ -28,3 +28,5 @@ fix foo (A : Type) (l : list A) {struct l} : option A :=
      : forall A : Type, list A -> option A
 
 Argument scopes are [type_scope list_scope]
+foo' = if A 0 then true else false
+     : bool
diff --git a/test-suite/output/Cases.v b/test-suite/output/Cases.v
index 61f89d40..37ee71e9 100644
--- a/test-suite/output/Cases.v
+++ b/test-suite/output/Cases.v
@@ -33,3 +33,16 @@ Fixpoint foo (A:Type) (l:list A) : option A :=
   end.
 
 Print foo.
+
+(* Do not duplicate the matched term *)
+
+Axiom A : nat -> bool.
+
+Definition foo' :=
+  match A 0 with
+    | true => true
+    | x => x
+  end.
+
+Print foo'.
+
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index 2066a7ef..42858304 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -50,3 +50,10 @@ Nil
      : forall A : Type, list A
 NIL:list nat
      : list nat
+Defining 'I' as keyword
+(false && I 3)%bool /\ I 6
+     : Prop
+[|1, 2, 3; 4, 5, 6|]
+     : Z * Z * Z * (Z * Z * Z)
+fun f : Z -> Z -> Z -> Z => {|f; 0; 1; 2|}:Z
+     : (Z -> Z -> Z -> Z) -> Z
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 6e637aca..b37c3638 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -129,3 +129,33 @@ Check Nil.
 
 Notation NIL := nil.
 Check NIL : list nat.
+
+
+(**********************************************************************)
+(* Test printing of notation with coercions in scope of a coercion    *)
+
+Open Scope nat_scope.
+
+Coercion is_true := fun b => b=true.
+Coercion of_nat n := match n with 0 => true | _ => false end.
+Notation "'I' x" := (of_nat (S x) || true)%bool (at level 10).
+
+Check (false && I 3)%bool /\ I 6.
+
+(**********************************************************************)
+(* Check notations with several recursive patterns                    *)
+
+Open Scope Z_scope.
+
+Notation "[| x , y , .. , z ; a , b , .. , c |]" :=
+  (pair (pair .. (pair x y) .. z) (pair .. (pair a b) .. c)).
+Check [|1,2,3;4,5,6|].
+
+(**********************************************************************)
+(* Test recursive notations involving applications                    *)
+(* Caveat: does not work for applied constant because constants are   *)
+(* classified as notations for the particular constant while this     *)
+(* generic application notation is classified as generic              *)
+
+Notation "{| f ; x ; .. ; y |}" := ( .. (f x) .. y).
+Check fun f => {| f; 0; 1; 2 |} : Z.
diff --git a/test-suite/success/Equations.v b/test-suite/success/Equations.v
new file mode 100644
index 00000000..e31135c2
--- /dev/null
+++ b/test-suite/success/Equations.v
@@ -0,0 +1,321 @@
+Require Import Program.
+
+Equations neg (b : bool) : bool :=
+neg true := false ;
+neg false := true.
+ 
+Eval compute in neg.
+
+Require Import Coq.Lists.List.
+
+Equations head A (default : A) (l : list A) : A :=
+head A default nil := default ;
+head A default (cons a v) := a.
+
+Eval compute in head.
+
+Equations tail {A} (l : list A) : (list A) :=
+tail A nil := nil ;
+tail A (cons a v) := v.
+
+Eval compute in @tail.
+
+Eval compute in (tail (cons 1 nil)).
+
+Reserved Notation " x ++ y " (at level 60, right associativity).
+
+Equations app' {A} (l l' : list A) : (list A) :=
+app' A nil l := l ;
+app' A (cons a v) l := cons a (app' v l).
+
+Equations app (l l' : list nat) : list nat :=
+  [] ++ l       := l ;
+  (a :: v) ++ l := a :: (v ++ l) 
+
+where " x ++ y " := (app x y).
+
+Eval compute in @app'.
+
+Equations zip' {A} (f : A -> A -> A) (l l' : list A) : (list A) :=
+zip' A f nil nil := nil ;
+zip' A f (cons a v) (cons b w) := cons (f a b) (zip' f v w) ;
+zip' A f nil (cons b w) := nil ;
+zip' A f (cons a v) nil := nil.
+
+
+Eval compute in @zip'.
+
+Equations zip'' {A} (f : A -> A -> A) (l l' : list A) (def : list A) : (list A) :=
+zip'' A f nil nil def := nil ;
+zip'' A f (cons a v) (cons b w) def := cons (f a b) (zip'' f v w def) ;
+zip'' A f nil (cons b w) def := def ;
+zip'' A f (cons a v) nil def := def.
+
+Eval compute in @zip''.
+
+Inductive fin : nat -> Set :=
+| fz : Π {n}, fin (S n)
+| fs : Π {n}, fin n -> fin (S n).
+
+Inductive finle : Π (n : nat) (x : fin n) (y : fin n), Prop :=
+| leqz : Π {n j}, finle (S n) fz j
+| leqs : Π {n i j}, finle n i j -> finle (S n) (fs i) (fs j).
+
+Scheme finle_ind_dep := Induction for finle Sort Prop.
+
+Instance finle_ind_pack n x y : DependentEliminationPackage (finle n x y) :=
+  { elim_type := _ ; elim := finle_ind_dep }.
+
+Implicit Arguments finle [[n]].
+
+Require Import Bvector.
+
+Implicit Arguments Vnil [[A]].
+Implicit Arguments Vcons [[A] [n]].
+
+Equations vhead {A n} (v : vector A (S n)) : A := 
+vhead A n (Vcons a v) := a.
+
+Equations vmap {A B} (f : A -> B) {n} (v : vector A n) : (vector B n) :=
+vmap A B f 0 Vnil := Vnil ;
+vmap A B f (S n) (Vcons a v) := Vcons (f a) (vmap f v).
+
+Eval compute in (vmap id (@Vnil nat)).
+Eval compute in (vmap id (@Vcons nat 2 _ Vnil)).
+Eval compute in @vmap.
+
+Equations Below_nat (P : nat -> Type) (n : nat) : Type :=
+Below_nat P 0 := unit ;
+Below_nat P (S n) := prod (P n) (Below_nat P n).
+
+Equations below_nat (P : nat -> Type) n (step : Π (n : nat), Below_nat P n -> P n) : Below_nat P n :=
+below_nat P 0 step := tt ;
+below_nat P (S n) step := let rest := below_nat P n step in
+  (step n rest, rest).
+
+Class BelowPack (A : Type) :=
+  { Below : Type ; below : Below }.
+
+Instance nat_BelowPack : BelowPack nat :=
+  { Below := Π P n step, Below_nat P n ;
+    below := λ P n step, below_nat P n (step P) }.
+
+Definition rec_nat (P : nat -> Type) n (step : Π n, Below_nat P n -> P n) : P n :=
+  step n (below_nat P n step).
+
+Fixpoint Below_vector (P : Π A n, vector A n -> Type) A n (v : vector A n) : Type :=
+  match v with Vnil => unit | Vcons a n' v' => prod (P A n' v') (Below_vector P A n' v') end.
+
+Equations below_vector (P : Π A n, vector A n -> Type) A n (v : vector A n)
+  (step : Π A n (v : vector A n), Below_vector P A n v -> P A n v) : Below_vector P A n v :=
+below_vector P A ?(0) Vnil step := tt ;
+below_vector P A ?(S n) (Vcons a v) step := 
+  let rest := below_vector P A n v step in
+    (step A n v rest, rest).
+
+Instance vector_BelowPack : BelowPack (Π A n, vector A n) :=
+  { Below := Π P A n v step, Below_vector P A n v ;
+    below := λ P A n v step, below_vector P A n v (step P) }.
+
+Instance vector_noargs_BelowPack A n : BelowPack (vector A n) :=
+  { Below := Π P v step, Below_vector P A n v ;
+    below := λ P v step, below_vector P A n v (step P) }.
+
+Definition rec_vector (P : Π A n, vector A n -> Type) A n v
+  (step : Π A n (v : vector A n), Below_vector P A n v -> P A n v) : P A n v :=
+  step A n v (below_vector P A n v step).
+
+Class Recursor (A : Type) (BP : BelowPack A) := 
+  { rec_type : Π x : A, Type ; rec : Π x : A, rec_type x }.
+
+Instance nat_Recursor : Recursor nat nat_BelowPack :=
+  { rec_type := λ n, Π P step, P n ;
+    rec := λ n P step, rec_nat P n (step P) }.
+
+(* Instance vect_Recursor : Recursor (Π A n, vector A n) vector_BelowPack := *)
+(*   rec_type := Π (P : Π A n, vector A n -> Type) step A n v, P A n v; *)
+(*   rec := λ P step A n v, rec_vector P A n v step. *)
+
+Instance vect_Recursor_noargs A n : Recursor (vector A n) (vector_noargs_BelowPack A n) :=
+  { rec_type := λ v, Π (P : Π A n, vector A n -> Type) step, P A n v;
+    rec := λ v P step, rec_vector P A n v step }.
+
+Implicit Arguments Below_vector [P A n].
+
+Notation " x ~= y " := (@JMeq _ x _ y) (at level 70, no associativity).
+
+(** Won't pass the guardness check which diverges anyway. *)
+
+(* Equations trans {n} {i j k : fin n} (p : finle i j) (q : finle j k) : finle i k := *)
+(* trans ?(S n) ?(fz) ?(j) ?(k) leqz q := leqz ; *)
+(* trans ?(S n) ?(fs i) ?(fs j) ?(fs k) (leqs p) (leqs q) := leqs (trans p q). *)
+
+(* Lemma trans_eq1 n (j k : fin (S n)) (q : finle j k) : trans leqz q = leqz. *)
+(* Proof. intros. simplify_equations ; reflexivity. Qed. *)
+
+(* Lemma trans_eq2 n i j k p q : @trans (S n) (fs i) (fs j) (fs k) (leqs p) (leqs q) = leqs (trans p q). *)
+(* Proof. intros. simplify_equations ; reflexivity. Qed. *)
+
+Section Image.
+  Context {S T : Type}.
+  Variable f : S -> T.
+  
+  Inductive Imf : T -> Type := imf (s : S) : Imf (f s).
+
+  Equations inv (t : T) (im : Imf t) : S :=
+  inv (f s) (imf s) := s.
+
+End Image.
+
+Section Univ.
+
+  Inductive univ : Set :=
+  | ubool | unat | uarrow (from:univ) (to:univ).
+
+  Equations interp (u : univ) : Type :=
+  interp ubool := bool ; interp unat := nat ; 
+  interp (uarrow from to) := interp from -> interp to.
+
+  Equations foo (u : univ) (el : interp u) : interp u :=
+  foo ubool true := false ;
+  foo ubool false := true ;
+  foo unat t := t ;
+  foo (uarrow from to) f := id ∘ f.
+
+  Eval lazy beta delta [ foo foo_obligation_1 foo_obligation_2 ] iota zeta in foo.
+
+End Univ.
+
+Eval compute in (foo ubool false).
+Eval compute in (foo (uarrow ubool ubool) negb).
+Eval compute in (foo (uarrow ubool ubool) id).
+
+Inductive foobar : Set := bar | baz.
+
+Equations bla (f : foobar) : bool :=
+bla bar := true ;
+bla baz := false.
+
+Eval simpl in bla.
+Print refl_equal.
+
+Notation "'refl'" := (@refl_equal _ _).
+
+Equations K {A} (x : A) (P : x = x -> Type) (p : P (refl_equal x)) (p : x = x) : P p :=
+K A x P p refl := p.
+
+Equations eq_sym {A} (x y : A) (H : x = y) : y = x :=
+eq_sym A x x refl := refl.
+
+Equations eq_trans {A} (x y z : A) (p : x = y) (q : y = z) : x = z :=
+eq_trans A x x x refl refl := refl.
+
+Lemma eq_trans_eq A x : @eq_trans A x x x refl refl = refl.
+Proof. reflexivity. Qed.
+
+Equations nth {A} {n} (v : vector A n) (f : fin n) : A :=
+nth A (S n) (Vcons a v) fz := a ;
+nth A (S n) (Vcons a v) (fs f) := nth v f.
+
+Equations tabulate {A} {n} (f : fin n -> A) : vector A n :=
+tabulate A 0 f := Vnil ;
+tabulate A (S n) f := Vcons (f fz) (tabulate (f ∘ fs)).
+
+Equations vlast {A} {n} (v : vector A (S n)) : A :=
+vlast A 0 (Vcons a Vnil) := a ;
+vlast A (S n) (Vcons a (n:=S n) v) := vlast v.
+
+Print Assumptions vlast.
+
+Equations vlast' {A} {n} (v : vector A (S n)) : A :=
+vlast' A ?(0) (Vcons a Vnil) := a ;
+vlast' A ?(S n) (Vcons a (n:=S n) v) := vlast' v.
+
+Lemma vlast_equation1 A (a : A) : vlast' (Vcons a Vnil) = a.
+Proof. intros. simplify_equations. reflexivity. Qed.
+
+Lemma vlast_equation2 A n a v : @vlast' A (S n) (Vcons a v) = vlast' v.
+Proof. intros. simplify_equations ; reflexivity. Qed.
+
+Print Assumptions vlast'.
+Print Assumptions nth. 
+Print Assumptions tabulate.
+
+Extraction vlast.
+Extraction vlast'.
+
+Equations vliat {A} {n} (v : vector A (S n)) : vector A n :=
+vliat A 0 (Vcons a Vnil) := Vnil ;
+vliat A (S n) (Vcons a v) := Vcons a (vliat v).
+
+Eval compute in (vliat (Vcons 2 (Vcons 5 (Vcons 4 Vnil)))).
+
+Equations vapp' {A} {n m} (v : vector A n) (w : vector A m) : vector A (n + m) :=
+vapp' A ?(0) m Vnil w := w ;
+vapp' A ?(S n) m (Vcons a v) w := Vcons a (vapp' v w).
+
+Eval compute in @vapp'.
+
+Fixpoint vapp {A n m} (v : vector A n) (w : vector A m) : vector A (n + m) :=
+  match v with
+    | Vnil => w
+    | Vcons a n' v' => Vcons a (vapp v' w)
+  end.
+
+Lemma JMeq_Vcons_inj A n m a (x : vector A n) (y : vector A m) : n = m -> JMeq x y -> JMeq (Vcons a x) (Vcons a y).
+Proof. intros until y. simplify_dep_elim. reflexivity. Qed.
+
+Equations NoConfusion_fin (P : Prop) {n : nat} (x y : fin n) : Prop :=
+NoConfusion_fin P (S n) fz fz := P -> P ;
+NoConfusion_fin P (S n) fz (fs y) := P ;
+NoConfusion_fin P (S n) (fs x) fz := P ;
+NoConfusion_fin P (S n) (fs x) (fs y) := (x = y -> P) -> P.
+
+Eval compute in NoConfusion_fin.
+Eval compute in NoConfusion_fin_comp.
+
+Print Assumptions NoConfusion_fin.
+
+Eval compute in (fun P n => NoConfusion_fin P (n:=S n) fz fz).
+
+(* Equations noConfusion_fin P (n : nat) (x y : fin n) (H : x = y) : NoConfusion_fin P x y := *)
+(* noConfusion_fin P (S n) fz fz refl := λ p _, p ; *)
+(* noConfusion_fin P (S n) (fs x) (fs x) refl := λ p : x = x -> P, p refl. *)
+
+Equations_nocomp NoConfusion_vect (P : Prop) {A n} (x y : vector A n) : Prop :=
+NoConfusion_vect P A 0 Vnil Vnil := P -> P ;
+NoConfusion_vect P A (S n) (Vcons a x) (Vcons b y) := (a = b -> x = y -> P) -> P.
+
+Equations noConfusion_vect (P : Prop) A n (x y : vector A n) (H : x = y) : NoConfusion_vect P x y :=
+noConfusion_vect P A 0 Vnil Vnil refl := λ p, p ;
+noConfusion_vect P A (S n) (Vcons a v) (Vcons a v) refl := λ p : a = a -> v = v -> P, p refl refl.
+
+(* Instance fin_noconf n : NoConfusionPackage (fin n) := *)
+(*   NoConfusion := λ P, Π x y, x = y -> NoConfusion_fin P x y ; *)
+(*   noConfusion := λ P x y, noConfusion_fin P n x y. *)
+
+Instance vect_noconf A n : NoConfusionPackage (vector A n) :=
+  { NoConfusion := λ P, Π x y, x = y -> NoConfusion_vect P x y ;
+    noConfusion := λ P x y, noConfusion_vect P A n x y }.
+
+Equations fog {n} (f : fin n) : nat :=
+fog (S n) fz := 0 ; fog (S n) (fs f) := S (fog f).
+
+Inductive Split {X : Set}{m n : nat} : vector X (m + n) -> Set :=
+  append : Π (xs : vector X m)(ys : vector X n), Split (vapp xs ys).
+
+Implicit Arguments Split [[X]].
+
+Equations_nocomp split {X : Set}(m n : nat) (xs : vector X (m + n)) : Split m n xs :=
+split X 0    n xs := append Vnil xs ;
+split X (S m) n (Vcons x xs) :=
+ let 'append xs' ys' in Split _ _ vec := split m n xs return Split (S m) n (Vcons x vec) in
+    append (Vcons x xs') ys'.
+
+Eval compute in (split 0 1 (vapp Vnil (Vcons 2 Vnil))).
+Eval compute in (split _ _ (vapp (Vcons 3 Vnil) (Vcons 2 Vnil))).
+
+Extraction Inline split_obligation_1 split_obligation_2.
+Recursive Extraction split.
+
+Eval compute in @split.
diff --git a/test-suite/success/Generalization.v b/test-suite/success/Generalization.v
new file mode 100644
index 00000000..6b503e95
--- /dev/null
+++ b/test-suite/success/Generalization.v
@@ -0,0 +1,13 @@
+
+Check `(a = 0).
+Check `(a = 0)%type.
+Definition relation A := A -> A -> Prop.
+Definition equivalence `(R : relation A) := True.
+Check (`(@equivalence A R)).
+
+Definition a_eq_b : `( a = 0 /\ a = b /\ b > c \/ d = e /\ d = 1).
+Admitted.
+Print a_eq_b.
+
+
+
diff --git a/test-suite/success/Inversion.v b/test-suite/success/Inversion.v
index f83328e8..b08ffcc3 100644
--- a/test-suite/success/Inversion.v
+++ b/test-suite/success/Inversion.v
@@ -99,3 +99,11 @@ Lemma depinv : forall a b, foo a b -> True.
 intros a b H.
 inversion H.
 Abort.
+
+(* Check non-regression of bug #1968 *)
+
+Inductive foo2 : option nat -> Prop := Foo : forall t, foo2 (Some t).
+Goal forall o, foo2 o -> 0 = 1.
+intros.
+eapply trans_eq. 
+inversion H.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 6dce0401..4bdd579a 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -26,3 +26,8 @@ Notation "x +1" := (S x) (at level 8, right associativity).
    right order *)
 
 Notation "' 'C_' G ( A )" := (A,G) (at level 8, G at level 2).
+
+(* Check import of notations from within a section *)
+
+Notation "+1 x" := (S x) (at level 25, x at level 9).
+Section A. Global Notation "'Z'" := O (at level 9). End A.
diff --git a/test-suite/success/Record.v b/test-suite/success/Record.v
index 7fdbcda7..885fff48 100644
--- a/test-suite/success/Record.v
+++ b/test-suite/success/Record.v
@@ -1,3 +1,82 @@
 (* Nijmegen expects redefinition of sorts *)
 Definition CProp := Prop.
-Record test : CProp :=  {n : nat}.
+Record test : CProp :=  {n : nat ; m : bool ; _ : n <> 0 }.
+Require Import Program.
+Require Import List.
+
+Record vector {A : Type} {n : nat} := { vec_list : list A ; vec_len : length vec_list = n }.
+Implicit Arguments vector [].
+
+Coercion vec_list : vector >-> list.
+
+Hint Rewrite @vec_len : datatypes.
+
+Ltac crush := repeat (program_simplify ; autorewrite with list datatypes ; auto with *).
+
+Obligation Tactic := crush.
+
+Program Definition vnil {A} : vector A 0 := {| vec_list := [] |}.
+
+Program Definition vcons {A n} (a : A) (v : vector A n) : vector A (S n) := 
+  {| vec_list := cons a (vec_list v) |}.
+
+Hint Rewrite map_length rev_length : datatypes.
+
+Program Definition vmap {A B n} (f : A -> B) (v : vector A n) : vector B n := 
+  {| vec_list := map f v |}.
+
+Program Definition vreverse {A n} (v : vector A n) : vector A n := 
+  {| vec_list := rev v |}.
+
+Fixpoint va_list {A B} (v : list (A -> B)) (w : list A) : list B := 
+  match v, w with
+    | nil, nil => nil
+    | cons f fs, cons x xs => cons (f x) (va_list fs xs)
+    | _, _ => nil
+  end.
+
+Program Definition va {A B n} (v : vector (A -> B) n) (w : vector A n) : vector B n := 
+  {| vec_list := va_list v w |}.
+
+Next Obligation. 
+  destruct v as [v Hv]; destruct w as [w Hw] ; simpl.
+  subst n. revert w Hw. induction v ; destruct w ; crush. 
+  rewrite IHv ; auto.
+Qed.
+
+(* Correct type inference of record notation. Initial example by Spiwack. *) 
+
+Inductive Machin := {
+ Bazar : option Machin
+}.
+
+Definition bli : Machin :=
+ {| Bazar := Some ({| Bazar := None |}:Machin) |}.
+
+Definition bli' : option (option Machin)  :=
+ Some (Some {| Bazar := None |} ).
+
+Definition bli'' : Machin :=
+ {| Bazar := Some {| Bazar := None |} |}.
+
+Definition bli''' := {| Bazar := Some {| Bazar := None |} |}.
+
+(** Correctly use scoping information *)
+
+Require Import ZArith.
+
+Record Foo := { bar : Z }.
+Definition foo := {| bar := 0 |}.
+
+(** Notations inside records *)
+
+Require Import Relation_Definitions.
+
+Record DecidableOrder : Type :=
+{ A : Type
+; le : relation A where "x <= y" := (le x y)
+; le_refl : reflexive _ le
+; le_antisym : antisymmetric _ le
+; le_trans : transitive _ le
+; le_total : forall x y, {x <= y}+{y <= x}
+}.
diff --git a/test-suite/success/Reordering.v b/test-suite/success/Reordering.v
new file mode 100644
index 00000000..de9b9975
--- /dev/null
+++ b/test-suite/success/Reordering.v
@@ -0,0 +1,15 @@
+(* Testing the reordering of hypothesis required by pattern, fold and change. *)
+Goal forall (A:Set) (x:A) (A':=A), True.
+intros.
+fold A' in x. (* suceeds: x is moved after A' *)
+Undo.
+pattern A' in x.
+Undo.
+change A' in x.
+Abort.
+
+(* p and m should be moved before H *)
+Goal forall n:nat, n=n -> forall m:nat, let p := (m,n) in True.
+intros.
+change n with (snd p) in H.
+Abort.
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index fcce68b9..952890ee 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -12,6 +12,44 @@ intros; apply Znot_le_gt, Zgt_lt in H.
 apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto.
 Qed.
 
+(* Test application under tuples *)
+
+Goal (forall x, x=0 <-> 0=x) -> 1=0 -> 0=1.
+intros H H'.
+apply H in H'.
+exact H'.
+Qed.
+
+(* Test as clause *)
+
+Goal (forall x, x=0 <-> (0=x /\ True)) -> 1=0 -> True.
+intros H H'.
+apply H in H' as (_,H').
+exact H'.
+Qed.
+
+(* Test application modulo conversion *)
+
+Goal (forall x, id x = 0 -> 0 = x) -> 1 = id 0 -> 0 = 1.
+intros H H'.
+apply H in H'.
+exact H'.
+Qed.
+
+(* Check apply/eapply distinction in presence of open terms *)
+
+Parameter h : forall x y z : nat, x = z -> x = y.
+Implicit Arguments h [[x] [y]].
+Goal 1 = 0 -> True.
+intro H.
+apply h in H || exact I.
+Qed.
+
+Goal False -> 1 = 0.
+intro H.
+apply h || contradiction.
+Qed.
+
 (* Check if it unfolds when there are not enough premises *)
 
 Goal forall n, n = S n -> False.
@@ -201,3 +239,18 @@ Axiom silly_axiom : forall v : exp, v = v -> False.
 Lemma silly_lemma : forall x : atom, False.
 intros x.
 apply silly_axiom with (v := x).  (* fails *)
+
+(* Test non-regression of (temporary) bug 1981 *)
+
+Goal exists n : nat, True.
+eapply ex_intro.
+exact O.
+trivial.
+Qed.
+
+(* Test non-regression of (temporary) bug 1980 *)
+
+Goal True.
+try eapply ex_intro.
+trivial.
+Qed.
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 48255386..488b057f 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -1,10 +1,10 @@
 Require Import Coq.Program.Program.
-Set Implicit Arguments.
-Unset Strict Implicit.
+Set Manual Implicit Arguments.
+
 
 Variable A : Set.
 
-Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall n, vector n -> vector (S n).
+Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall {n}, vector n -> vector (S n).
 
 Goal forall n, forall v : vector (S n), vector n.
 Proof.
@@ -35,51 +35,55 @@ Inductive ctx : Type :=
 | empty : ctx
 | snoc : ctx -> type -> ctx.
 
-Notation " Γ , τ " := (snoc Γ τ) (at level 25, t at next level, left associativity).
+Bind Scope context_scope with ctx.
+Delimit Scope context_scope with ctx.
+
+Arguments Scope snoc [context_scope].
+
+Notation " Γ ,, τ " := (snoc Γ τ) (at level 25, t at next level, left associativity).
 
-Fixpoint conc (Γ Δ : ctx) : ctx :=
+Fixpoint conc (Δ Γ : ctx) : ctx :=
   match Δ with
     | empty => Γ
-    | snoc Δ' x => snoc (conc Γ Δ') x
+    | snoc Δ' x => snoc (conc Δ' Γ) x
   end.
 
-Notation " Γ ; Δ " := (conc Γ Δ) (at level 25, left associativity).
+Notation " Γ ;; Δ " := (conc Δ Γ) (at level 25, left associativity) : context_scope.
 
 Inductive term : ctx -> type -> Type :=
-| ax : forall Γ τ, term (Γ, τ) τ
-| weak : forall Γ τ, term Γ τ -> forall τ', term (Γ, τ') τ
-| abs : forall Γ τ τ', term (Γ , τ) τ' -> term Γ (τ --> τ')
+| ax : forall Γ τ, term (snoc Γ τ) τ
+| weak : forall Γ τ, term Γ τ -> forall τ', term (Γ ,, τ') τ
+| abs : forall Γ τ τ', term (snoc Γ τ) τ' -> term Γ (τ --> τ')
 | app : forall Γ τ τ', term Γ (τ --> τ') -> term Γ τ -> term Γ τ'.
 
-Lemma weakening : forall Γ Δ τ, term (Γ ; Δ) τ -> 
-  forall τ', term (Γ , τ' ; Δ) τ.
-Proof with simpl in * ; auto ; simpl_depind.
+Hint Constructors term : lambda.
+
+Open Local Scope context_scope.
+
+Notation " Γ |-- τ " := (term Γ τ) (at level 0) : type_scope.
+
+Lemma weakening : forall Γ Δ τ, term (Γ ;; Δ) τ -> 
+  forall τ', term (Γ ,, τ' ;; Δ) τ.
+Proof with simpl in * ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; eauto with lambda.
   intros Γ Δ τ H.
 
   dependent induction H.
 
   destruct Δ...
-    apply weak ; apply ax.
-    
-    apply ax.
-    
-  destruct Δ...
-    specialize (IHterm Γ empty)... 
-    apply weak...
-
-    apply weak...
 
   destruct Δ...
-    apply weak ; apply abs ; apply H.
 
+  destruct Δ...
     apply abs...
-    specialize (IHterm Γ0 (Δ, t, τ))...
+    
+    specialize (IHterm (Δ,, t,, τ)%ctx Γ0)...
 
+  intro.
   apply app with τ...
 Qed.
 
-Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ.
-Proof with simpl in * ; simpl_depind ; auto.
+Lemma exchange : forall Γ Δ α β τ, term (Γ,, α,, β ;; Δ) τ -> term (Γ,, β,, α ;; Δ) τ.
+Proof with simpl in * ; subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps ; auto.
   intros until 1.
   dependent induction H.
 
@@ -89,12 +93,37 @@ Proof with simpl in * ; simpl_depind ; auto.
     apply ax.
 
   destruct Δ...
-    pose (weakening (Γ:=Γ0) (Δ:=(empty, α)))...
+    pose (weakening Γ0 (empty,, α))...
 
     apply weak...
 
-  apply abs...
-  specialize (IHterm Γ0 α β (Δ, τ))...
+  apply abs... 
+  specialize (IHterm (Δ ,, τ))...
 
   eapply app with τ...
 Save.
+
+(** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *)
+
+Unset Manual Implicit Arguments.
+
+Inductive Ty :=
+ | Nat : Ty
+ | Prod : Ty -> Ty -> Ty.
+
+Inductive Exp : Ty -> Type :=
+| Const : nat -> Exp Nat
+| Pair : forall t1 t2, Exp t1 -> Exp t2 -> Exp (Prod t1 t2)
+| Fst : forall t1 t2, Exp (Prod t1 t2) -> Exp t1.
+
+Inductive Ev : forall t, Exp t -> Exp t -> Prop :=
+| EvConst   : forall n, Ev (Const n) (Const n)
+| EvPair    : forall t1 t2 (e1:Exp t1) (e2:Exp t2) e1' e2',
+               Ev e1 e1' -> Ev e2 e2' -> Ev (Pair e1 e2) (Pair e1' e2')
+| EvFst     : forall t1 t2 (e:Exp (Prod t1 t2)) e1 e2,
+               Ev e (Pair e1 e2) ->
+               Ev (Fst e) e1.
+
+Lemma EvFst_inversion : forall t1 t2 (e:Exp (Prod t1 t2)) e1, Ev (Fst e) e1 -> exists e2, Ev e (Pair e1 e2).
+intros t1 t2 e e1 ev. dependent destruction ev. exists e2 ; assumption. 
+Qed.
diff --git a/test-suite/success/guard.v b/test-suite/success/guard.v
new file mode 100644
index 00000000..b9181d43
--- /dev/null
+++ b/test-suite/success/guard.v
@@ -0,0 +1,11 @@
+(* Specific tests about guard condition *)
+
+(* f must unfold to x, not F (de Bruijn mix-up!) *)
+Check let x (f:nat->nat) k := f k in
+      fun (y z:nat->nat) =>
+      let f:=x in (* f := Rel 3 *)
+      fix F (n:nat) : nat :=
+        match n with
+        | 0 => 0
+        | S k => f F k (* here Rel 3 = F ! *)
+        end.
diff --git a/test-suite/success/refine.v b/test-suite/success/refine.v
index 4b636618..b654277c 100644
--- a/test-suite/success/refine.v
+++ b/test-suite/success/refine.v
@@ -117,3 +117,8 @@ refine
 	let fn := fact_rec (n-1) _ in
         n * fn).
 Abort.
+
+(* Wish 1988: that fun forces unfold in refine *)
+
+Goal (forall A : Prop, A -> ~~A).
+Proof. refine(fun A a f => _).
diff --git a/test-suite/success/rewrite_iterated.v b/test-suite/success/rewrite_iterated.v
new file mode 100644
index 00000000..962dada3
--- /dev/null
+++ b/test-suite/success/rewrite_iterated.v
@@ -0,0 +1,30 @@
+Require Import Arith Omega.
+
+Lemma test : forall p:nat, p<>0 -> p-1+1=p.
+Proof.
+ intros; omega.
+Qed.
+
+(** Test of new syntax for rewrite : ! ? and so on... *)
+
+Lemma but : forall a b c, a<>0 -> b<>0 -> c<>0 ->
+ (a-1+1)+(b-1+1)+(c-1+1)=a+b+c.
+Proof.
+intros.
+rewrite test.
+Undo.
+rewrite test,test.
+Undo.
+rewrite 2 test. (* or rewrite 2test or rewrite 2!test *)
+Undo.
+rewrite 2!test,2?test.
+Undo.
+(*rewrite 4!test.  --> error *)
+rewrite 3!test.
+Undo.
+rewrite <- 3?test.
+Undo.
+(*rewrite <-?test. --> loops*)
+rewrite !test by auto.
+reflexivity.
+Qed.
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index f49f58e5..be5999df 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -116,3 +116,17 @@ Add Morphism (@f A) : f_morph.
 Proof.
 unfold rel, f. trivial.
 Qed.
+
+(* Submitted by Nicolas Tabareau *)
+(* Needs unification.ml to support environments with de Bruijn *)
+
+Goal forall
+  (f : Prop -> Prop)
+  (Q : (nat -> Prop) -> Prop)
+  (H : forall (h : nat -> Prop), Q (fun x : nat => f (h x)) <-> True)
+  (h:nat -> Prop), 
+  Q (fun x : nat => f (Q (fun b : nat => f (h x)))) <-> True.
+intros f0 Q H.
+setoid_rewrite H.
+tauto.
+Qed.
diff --git a/test-suite/success/simpl.v b/test-suite/success/simpl.v
index 8d32b1d9..b4de4932 100644
--- a/test-suite/success/simpl.v
+++ b/test-suite/success/simpl.v
@@ -21,4 +21,27 @@ with copy_of_compute_size_tree (t:tree) : nat :=
 Eval simpl in (copy_of_compute_size_forest leaf).
 
 
+(* Another interesting case: Hrec has to occurrences: one cannot be folded
+   back to f while the second can. *)
+Parameter g : (nat->nat)->nat->nat->nat.
 
+Definition f (n n':nat) :=
+  nat_rec (fun _ => nat -> nat)
+    (fun x => x)
+    (fun k Hrec => g Hrec (Hrec k))
+    n n'.
+
+Goal forall a b, f (S a) b = b.
+intros.
+simpl.
+admit.
+Qed. (* Qed will fail if simpl performs eta-expansion *)
+
+(* Yet another example. *)
+
+Require Import List.
+
+Goal forall A B (a:A) l f (i:B), fold_right f i ((a :: l))=i.
+simpl.
+admit.
+Qed. (* Qed will fail if simplification is incorrect (de Bruijn!) *)
diff --git a/test-suite/success/unicode_utf8.v b/test-suite/success/unicode_utf8.v
index 19e306fe..8b7764e5 100644
--- a/test-suite/success/unicode_utf8.v
+++ b/test-suite/success/unicode_utf8.v
@@ -1,12 +1,104 @@
-(* Check correct separation of identifiers followed by unicode symbols *)
-  Notation "x 〈 w" := (plus x w) (at level 30).
-  Check fun x => x〈x.
+(** PARSER TESTS *)
 
-(* Check Greek letters *)
+(** Check correct separation of identifiers followed by unicode symbols *)
+Notation "x ⊕ w" := (plus x w) (at level 30).
+Check fun x => x⊕x.
+
+(** Check Greek letters *)
 Definition test_greek : nat -> nat := fun Δ => Δ.
 Parameter ℝ : Set.
 Parameter π : ℝ.
 
-(* Check indices *)
+(** Check indices *)
 Definition test_indices : nat -> nat := fun x₁ => x₁.
 Definition π₂ := snd.
+
+(** More unicode in identifiers *)
+Definition αβ_áà_אב := 0.
+
+
+(** UNICODE IN STRINGS *)
+
+Require Import List Ascii String.
+Open Scope string_scope.
+
+Definition test_string := "azertyαβ∀ééé".
+Eval compute in length test_string.
+ (** last six "chars" are unicode, hence represented by 2 bytes,
+     except the forall which is 3 bytes *)
+
+Fixpoint string_to_list s :=
+  match s with
+    | EmptyString => nil
+    | String c s => c :: string_to_list s
+  end.
+
+Eval compute in (string_to_list test_string).
+ (** for instance, α is \206\177 whereas ∀ is \226\136\128 *)
+Close Scope string_scope.
+
+
+
+(** INTERFACE TESTS *)
+
+Require Import Utf8.
+
+(** Printing of unicode notation, in *goals* *)
+Lemma test : forall A:Prop, A -> A.
+Proof.
+auto.
+Qed.
+
+(** Parsing of unicode notation, in *goals* *)
+Lemma test2 : ∀A:Prop, A → A.
+Proof.
+intro.
+intro.
+auto.
+Qed.
+
+(** Printing of unicode notation, in *response* *)
+Check fun (X:Type)(x:X) => x.
+
+(** Parsing of unicode notation, in *response* *)
+Check ∀Δ, Δ → Δ.
+Check ∀x, x=0 ∨ x=0 → x=0.
+
+
+(** ISSUES: *)
+
+Notation "x ≠ y" := (x<>y) (at level 70).
+
+Notation "x ≤ y" := (x<=y) (at level 70, no associativity).
+
+(** First Issue : ≤ is attached to "le" of nat, not to notation <= *)
+
+Require Import ZArith.
+Open Scope Z_scope.
+Locate "≤". (* still le, not Zle *)
+Notation "x ≤ y" := (x<=y) (at level 70, no associativity).
+Locate "≤".
+Close Scope Z_scope.
+
+(** ==> How to proceed modularly ? *)
+
+
+(** Second Issue : notation for -> generates useless parenthesis
+   if followed by a binder *)
+
+Check 0≠0 → ∀x:nat,x=x.
+
+(** Example of real situation : *)
+
+Definition pred : ∀x, x≠0 → ∃y, x = S y.
+Proof.
+destruct x.
+destruct 1; auto.
+intros _.
+exists x; auto.
+Defined.
+
+Print pred.
+
+
+