14 files changed, 733 insertions, 35 deletions

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.
+
+
+