Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2

22 files changed, 468 insertions, 169 deletions

diff --git a/test-suite/bugs/closed/shouldsucceed/2603.v b/test-suite/bugs/closed/shouldsucceed/2603.v
index a556b9bf..371bfdc5 100644
--- a/test-suite/bugs/closed/shouldsucceed/2603.v
+++ b/test-suite/bugs/closed/shouldsucceed/2603.v
@@ -1,3 +1,18 @@
+(** Namespace of module vs. namescope of definitions/constructors/...
+
+As noticed by A. Appel in bug #2603, module names and definition
+names used to be in the same namespace. But conflict with names
+of constructors (or 2nd mutual inductive...) used to not be checked
+enough, leading to stange situations.
+
+- In 8.3pl3 we introduced checks that forbid uniformly the following
+  situations.
+
+- For 8.4 we finally managed to make module names and other names
+  live in two separate namespace, hence allowing all of the following
+  situations.
+*)
+
 Module Type T.
 End T.
 
@@ -9,10 +24,10 @@ End L.
 
 Module M1 : L with Module E:=K.
 Module E := K.
-Fail Inductive t := E. (* Used to be accepted, but End M1 below was failing *)
+Inductive t := E. (* Used to be accepted, but End M1 below was failing *)
 End M1.
 
 Module M2 : L with Module E:=K.
 Inductive t := E.
-Fail Module E := K. (* Used to be accepted *)
-Fail End M2. (* Used to be accepted *)
+Module E := K. (* Used to be accepted *)
+End M2. (* Used to be accepted *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2732.v b/test-suite/bugs/closed/shouldsucceed/2732.v
new file mode 100644
index 00000000..f22a8ccc
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2732.v
@@ -0,0 +1,19 @@
+(* Check correct behavior of add_primitive_tactic in TACEXTEND *)
+
+(* Added also the case of eauto and congruence *)
+
+Ltac thus H := solve [H].
+
+Lemma test: forall n : nat, n <= n.
+Proof.
+  intro.
+  thus firstorder.
+  Undo.
+  thus eauto.
+Qed.
+
+Lemma test2: false = true -> False.
+Proof.
+  intro.
+  thus congruence.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/2733.v b/test-suite/bugs/closed/shouldsucceed/2733.v
new file mode 100644
index 00000000..fd7bd3bd
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2733.v
@@ -0,0 +1,26 @@
+Definition goodid : forall {A} (x: A), A := fun A x => x.
+Definition wrongid : forall A (x: A), A := fun {A} x => x.
+
+Inductive ty := N | B.
+
+Inductive alt_list : ty -> ty -> Type :=
+  | nil {k} : alt_list k k
+  | Ncons {k} : nat -> alt_list B k -> alt_list N k
+  | Bcons {k} : bool -> alt_list N k -> alt_list B k.
+
+Definition trullynul k {k'} (l : alt_list k k') :=
+match k,l with
+ |N,l' => Ncons 0 (Bcons true l')
+ |B,l' => Bcons true (Ncons 0 l')
+end.
+
+Fixpoint app (P : forall {k k'}, alt_list k k' -> alt_list k k') {t1 t2} (l : alt_list t1 t2) {struct l}: forall {t3}, alt_list t2 t3 ->
+alt_list t1 t3 :=
+  match l with
+  | nil _ => fun _ l2 => P l2
+  | Ncons _ n l1 => fun _ l2 => Ncons n (app (@P) l1 l2)
+  | Bcons _ b l1 => fun _ l2 => Bcons b (app (@P) l1 l2)
+  end.
+
+Check (fun {t t'} (l: alt_list t t') =>
+ app trullynul (goodid l) (wrongid _ nil)).
diff --git a/test-suite/complexity/autodecomp.v b/test-suite/complexity/autodecomp.v
deleted file mode 100644
index 85589ff7..00000000
--- a/test-suite/complexity/autodecomp.v
+++ /dev/null
@@ -1,11 +0,0 @@
-(* 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.
-
-Timeout 5 Time auto decomp.
diff --git a/test-suite/output/Arguments.out b/test-suite/output/Arguments.out
index 139f9e99..7c9b1e27 100644
--- a/test-suite/output/Arguments.out
+++ b/test-suite/output/Arguments.out
@@ -91,3 +91,11 @@ The simpl tactic unfolds f
   when the 5th, 6th and 7th arguments evaluate to a constructor 
 f is transparent
 Expands to: Constant Top.f
+forall w : r, w 3 true = tt
+     : Prop
+The command has indeed failed with message:
+=> Error: Unknown interpretation for notation "$".
+w 3 true = tt
+     : Prop
+The command has indeed failed with message:
+=> Error: Extra argument _.
diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v
index 3a94f19a..573cfdab 100644
--- a/test-suite/output/Arguments.v
+++ b/test-suite/output/Arguments.v
@@ -38,3 +38,15 @@ End S1.
 About f.
 Arguments f : clear implicits and scopes.
 About f.
+Record r := { pi :> nat -> bool -> unit }.
+Notation "$" := 3 (only parsing) : foo_scope.
+Notation "$" := true (only parsing) : bar_scope.
+Delimit Scope bar_scope with B.
+Arguments pi _ _%F _%B. 
+Check (forall w : r, pi w $ $ = tt).
+Fail Check (forall w : r, w $ $ = tt).
+Axiom w : r.
+Arguments w  _%F _%B : extra scopes.
+Check (w $ $ = tt).
+Fail Arguments w  _%F _%B.
+
diff --git a/test-suite/output/Notations2.out b/test-suite/output/Notations2.out
index 47741e43..cf45025e 100644
--- a/test-suite/output/Notations2.out
+++ b/test-suite/output/Notations2.out
@@ -10,6 +10,8 @@ end
      : nat
 let '(a, _, _) := (2, 3, 4) in a
      : nat
+exists myx (y : bool), myx = y
+     : Prop
 fun (P : nat -> nat -> Prop) (x : nat) => exists x0, P x x0
      : (nat -> nat -> Prop) -> nat -> Prop
 ∃ n p : nat, n + p = 0
@@ -46,3 +48,7 @@ match n with
 | plus2 _ :: _ => 2
 end
      : list(nat) -> nat
+# x : nat => x
+     : nat -> nat
+# _ : nat => 2
+     : nat -> nat
diff --git a/test-suite/output/Notations2.v b/test-suite/output/Notations2.v
index e902a3c2..e53c94ef 100644
--- a/test-suite/output/Notations2.v
+++ b/test-suite/output/Notations2.v
@@ -25,6 +25,11 @@ Remove Printing Let prod.
 Check match (0,0,0) with (x,y,z) => x+y+z end.
 Check let '(a,b,c) := ((2,3),4) in a.
 
+(* Check printing of notations with mixed reserved binders (see bug #2571) *)
+
+Implicit Type myx : bool.
+Check exists myx y, myx = y.
+
 (* Test notation for anonymous functions up to eta-expansion *)
 
 Check fun P:nat->nat->Prop => fun x:nat => ex (P x). 
@@ -83,3 +88,13 @@ Notation "'mylet' f [ x ; .. ; y ]  :=  t 'in' u":=
 
 Check mylet f [x;y;z;(a:bool)] := x+y+z+1 in f 0 1 2.
 *)
+
+(* Check notations for functional terms which do not necessarily
+   depend on their parameter *)
+(* Old request mentioned again on coq-club 20/1/2012 *)
+
+Notation "#  x : T => t" := (fun x : T => t)
+  (at level 0, t at level 200, x ident).
+
+Check # x : nat => x.
+Check # _ : nat => 2.
diff --git a/test-suite/output/PrintInfos.out b/test-suite/output/PrintInfos.out
index 40c786ab..598bb728 100644
--- a/test-suite/output/PrintInfos.out
+++ b/test-suite/output/PrintInfos.out
@@ -37,10 +37,11 @@ When applied to no arguments:
 When applied to 1 argument:
   Argument A is implicit
 plus = 
-fix plus (n m : nat) : nat := match n with
-                              | 0 => m
-                              | S p => S (plus p m)
-                              end
+fix plus (n m : nat) {struct n} : nat :=
+  match n with
+  | 0 => m
+  | S p => S (plus p m)
+  end
      : nat -> nat -> nat
 
 Argument scopes are [nat_scope nat_scope]
diff --git a/test-suite/success/Cases.v b/test-suite/success/Cases.v
index 745529bf..f445ca8e 100644
--- a/test-suite/success/Cases.v
+++ b/test-suite/success/Cases.v
@@ -100,7 +100,7 @@ Type (fun x : nat => match x return nat with
                      | x => x
                      end).
 
-Section testlist.
+Module Type testlist.
 Parameter A : Set.
 Inductive list : Set :=
   | nil : list
@@ -119,7 +119,6 @@ Definition titi (a : A) (l : list) :=
   | nil => l
   | cons b l => l
   end.
-Reset list.
 End testlist.
 
 
@@ -913,71 +912,77 @@ Type
    | LeS n m _ => (S n, S m)
    end).
 
-
+Module Type F_v1.
 Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) :=
   match h in (Le n m) return (Le n (S m)) with
   | LeO m' => LeO (S m')
   | LeS n' m' h' => LeS n' (S m') (F n' m' h')
   end.
+End F_v1.
 
-Reset F.
-
+Module Type F_v2.
 Fixpoint F (n m : nat) (h : Le n m) {struct h} : Le n (S m) :=
   match h in (Le n m) return (Le n (S m)) with
   | LeS n m h => LeS n (S m) (F n m h)
   | LeO m => LeO (S m)
   end.
+End F_v2.
 
 (* Rend la longueur de la liste *)
-Definition length1 (n : nat) (l : listn n) :=
+
+Module Type L1.
+Definition length (n : nat) (l : listn n) :=
   match l return nat with
   | consn n _ (consn m _ _) => S (S m)
   | consn n _ _ => 1
   | _ => 0
   end.
+End L1.
 
-Reset length1.
-Definition length1 (n : nat) (l : listn n) :=
+Module Type L1'.
+Definition length (n : nat) (l : listn n) :=
   match l with
   | consn n _ (consn m _ _) => S (S m)
   | consn n _ _ => 1
   | _ => 0
   end.
+End L1'.
 
-
-Definition length2 (n : nat) (l : listn n) :=
+Module Type L2.
+Definition length (n : nat) (l : listn n) :=
   match l return nat with
   | consn n _ (consn m _ _) => S (S m)
   | consn n _ _ => S n
   | _ => 0
   end.
+End L2.
 
-Reset length2.
-
-Definition length2 (n : nat) (l : listn n) :=
+Module Type L2'.
+Definition length (n : nat) (l : listn n) :=
   match l with
   | consn n _ (consn m _ _) => S (S m)
   | consn n _ _ => S n
   | _ => 0
   end.
+End L2'.
 
-Definition length3 (n : nat) (l : listn n) :=
+Module Type L3.
+Definition length (n : nat) (l : listn n) :=
   match l return nat with
   | consn n _ (consn m _ l) => S n
   | consn n _ _ => 1
   | _ => 0
   end.
+End L3.
 
-
-Reset length3.
-
-Definition length3 (n : nat) (l : listn n) :=
+Module Type L3'.
+Definition length (n : nat) (l : listn n) :=
   match l with
   | consn n _ (consn m _ l) => S n
   | consn n _ _ => 1
   | _ => 0
   end.
-
+End L3'.
 
 Type match LeO 0 return nat with
      | LeS n m h => n + m
@@ -1256,7 +1261,7 @@ Type match (0, 0) with
      | (x, y) => (S x, S y)
      end.
 
-
+Module Type test_concat.
 
 Parameter concat : forall A : Set, List A -> List A -> List A.
 
@@ -1273,6 +1278,7 @@ Type
   | _, _ => Nil nat
   end.
 
+End test_concat.
 
 Inductive redexes : Set :=
   | VAR : nat -> redexes
@@ -1295,7 +1301,6 @@ Type (fun n : nat => match n with
                      | _ => 0
                      end).
 
-Reset concat.
 Parameter
   concat :
     forall n : nat, listn n -> forall m : nat, listn m -> listn (n + m).
@@ -1383,6 +1388,7 @@ Type
 (* I.e. to test manipulation of elimination predicate                    *)
 (* ===================================================================== *)
 
+Module Type test_term.
 
 Parameter LTERM : nat -> Set.
 Inductive TERM : Type :=
@@ -1397,7 +1403,8 @@ Type
   | oper op1 l1, oper op2 l2 => False
   | _, _ => False
   end.
-Reset LTERM.
+
+End test_term.
 
 
 
@@ -1493,6 +1500,7 @@ Type
   end.
 
 
+Module Type ff.
 
 Parameter ff : forall n m : nat, n <> m -> S n <> S m.
 Parameter discr_r : forall n : nat, 0 <> S n.
@@ -1505,6 +1513,7 @@ Type
    | S x => or_intror (S x = 0) (discr_l x)
    end).
 
+Module Type eqdec.
 
 Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
   match n, m return (n = m \/ n <> m) with
@@ -1518,7 +1527,9 @@ Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
       end
   end.
 
-Reset eqdec.
+End eqdec.
+
+Module Type eqdec'.
 
 Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
   match n return (forall m : nat, n = m \/ n <> m) with
@@ -1540,6 +1551,7 @@ Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
       end
   end.
 
+End eqdec'.
 
 Inductive empty : forall n : nat, listn n -> Prop :=
     intro_empty : empty 0 niln.
@@ -1554,7 +1566,10 @@ Type
    | consn n a y as b => or_intror (empty (S n) b) (inv_empty n a y)
    end).
 
-Reset ff.
+End ff.
+
+Module Type ff'.
+
 Parameter ff : forall n m : nat, n <> m -> S n <> S m.
 Parameter discr_r : forall n : nat, 0 <> S n.
 Parameter discr_l : forall n : nat, S n <> 0.
@@ -1566,6 +1581,7 @@ Type
    | S x => or_intror (S x = 0) (discr_l x)
    end).
 
+Module Type eqdec.
 
 Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
   match n, m return (n = m \/ n <> m) with
@@ -1578,7 +1594,10 @@ Fixpoint eqdec (n m : nat) {struct n} : n = m \/ n <> m :=
       | or_intror h => or_intror (S x = S y) (ff x y h)
       end
   end.
-Reset eqdec.
+
+End eqdec.
+
+Module Type eqdec'.
 
 Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
   match n return (forall m : nat, n = m \/ n <> m) with
@@ -1600,6 +1619,8 @@ Fixpoint eqdec (n : nat) : forall m : nat, n = m \/ n <> m :=
       end
   end.
 
+End eqdec'.
+End ff'.
 
 (* ================================================== *)
 (* Pour tester parametres                             *)
diff --git a/test-suite/success/CasesDep.v b/test-suite/success/CasesDep.v
index d3b7cf3f..bfead53c 100644
--- a/test-suite/success/CasesDep.v
+++ b/test-suite/success/CasesDep.v
@@ -222,7 +222,7 @@ Definition Dposint := Build_DSetoid Set_of_posint Eq_posint_deci.
  de l'arite de chaque operateur *)
 
 
-Section Sig.
+Module Sig.
 
 Record Signature : Type :=
   {Sigma : DSetoid; Arity : Map (Set_of Sigma) (Set_of Dposint)}.
@@ -277,7 +277,7 @@ Type
   | _, _ => False
   end.
 
-
+Module Type Version1.
 
 Definition equalT (t1 t2 : TERM) : Prop :=
   match t1, t2 with
@@ -294,12 +294,15 @@ Definition EqListT (n1 : posint) (l1 : LTERM n1) (n2 : posint)
   | _, _ => False
   end.
 
+End Version1.
+
 
-Reset equalT.
 (* ------------------------------------------------------------------*)
 (*          Initial exemple (without patterns)                       *)
 (*-------------------------------------------------------------------*)
 
+Module Version2.
+
 Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
   match t1 return (TERM -> Prop) with
   | var v1 =>
@@ -347,11 +350,13 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
       end
   end.
 
+End Version2.
 
 (* ---------------------------------------------------------------- *)
 (*                Version with simple patterns                      *)
 (* ---------------------------------------------------------------- *)
-Reset equalT.
+
+Module Version3.
 
 Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
   match t1 with
@@ -388,8 +393,9 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
       end
   end.
 
+End Version3.
 
-Reset equalT.
+Module Version4.
 
 Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
   match t1 with
@@ -423,10 +429,13 @@ Fixpoint equalT (t1 : TERM) : TERM -> Prop :=
       end
   end.
 
+End Version4.
+
 (* ---------------------------------------------------------------- *)
 (*                  Version with multiple patterns                  *)
 (* ---------------------------------------------------------------- *)
-Reset equalT.
+
+Module Version5.
 
 Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop :=
   match t1, t2 with
@@ -445,6 +454,7 @@ Fixpoint equalT (t1 t2 : TERM) {struct t1} : Prop :=
   | _, _ => False
   end.
 
+End Version5.
 
 (* ------------------------------------------------------------------ *)
 
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index a93f8900..071fb957 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -16,11 +16,6 @@ Hint Immediate refl_equal sym_equal: foo.
 Hint Unfold fst sym_equal.
 Hint Unfold fst sym_equal: foo.
 
-(* What's this stranged syntax ? *)
-Hint Destruct h6 := 4 Conclusion (_ <= _) => fun H => apply H.
-Hint Destruct h7 := 4 Discardable Hypothesis (_ <= _) => fun H => apply H.
-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.
diff --git a/test-suite/success/Mod_params.v b/test-suite/success/Mod_params.v
index 74228bbb..51516166 100644
--- a/test-suite/success/Mod_params.v
+++ b/test-suite/success/Mod_params.v
@@ -20,59 +20,31 @@ End Q.
 #trace Nametab.exists_cci;;
 *)
 
-Module M.
-Reset M.
-Module M (X: SIG).
-Reset M.
-Module M (X Y: SIG).
-Reset M.
-Module M (X: SIG) (Y: SIG).
-Reset M.
-Module M (X Y: SIG) (Z1 Z: SIG).
-Reset M.
-Module M (X: SIG) (Y: SIG).
-Reset M.
-Module M (X Y: SIG) (Z1 Z: SIG).
-Reset M.
-Module M : SIG.
-Reset M.
-Module M (X: SIG) : SIG.
-Reset M.
-Module M (X Y: SIG) : SIG.
-Reset M.
-Module M (X: SIG) (Y: SIG) : SIG.
-Reset M.
-Module M (X Y: SIG) (Z1 Z: SIG) : SIG.
-Reset M.
-Module M (X: SIG) (Y: SIG) : SIG.
-Reset M.
-Module M (X Y: SIG) (Z1 Z: SIG) : SIG.
-Reset M.
-Module M := F Q.
-Reset M.
-Module M (X: FSIG) := X Q.
-Reset M.
-Module M (X Y: FSIG) := X Q.
-Reset M.
-Module M (X: FSIG) (Y: SIG) := X Y.
-Reset M.
-Module M (X Y: FSIG) (Z1 Z: SIG) := X Z.
-Reset M.
-Module M (X: FSIG) (Y: SIG) := X Y.
-Reset M.
-Module M (X Y: FSIG) (Z1 Z: SIG) := X Z.
-Reset M.
-Module M : SIG := F Q.
-Reset M.
-Module M (X: FSIG) : SIG := X Q.
-Reset M.
-Module M (X Y: FSIG) : SIG := X Q.
-Reset M.
-Module M (X: FSIG) (Y: SIG) : SIG := X Y.
-Reset M.
-Module M (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z.
-Reset M.
-Module M (X: FSIG) (Y: SIG) : SIG := X Y.
-Reset M.
-Module M (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z.
-Reset M.
+Module M01. End M01.
+Module M02 (X: SIG). End M02.
+Module M03 (X Y: SIG). End M03.
+Module M04 (X: SIG) (Y: SIG). End M04.
+Module M05 (X Y: SIG) (Z1 Z: SIG). End M05.
+Module M06 (X: SIG) (Y: SIG). End M06.
+Module M07 (X Y: SIG) (Z1 Z: SIG). End M07.
+Module M08 : SIG. End M08.
+Module M09 (X: SIG) : SIG. End M09.
+Module M10 (X Y: SIG) : SIG. End M10.
+Module M11 (X: SIG) (Y: SIG) : SIG. End M11.
+Module M12 (X Y: SIG) (Z1 Z: SIG) : SIG. End M12.
+Module M13 (X: SIG) (Y: SIG) : SIG. End M13.
+Module M14 (X Y: SIG) (Z1 Z: SIG) : SIG. End M14.
+Module M15 := F Q.
+Module M16 (X: FSIG) := X Q.
+Module M17 (X Y: FSIG) := X Q.
+Module M18 (X: FSIG) (Y: SIG) := X Y.
+Module M19 (X Y: FSIG) (Z1 Z: SIG) := X Z.
+Module M20 (X: FSIG) (Y: SIG) := X Y.
+Module M21 (X Y: FSIG) (Z1 Z: SIG) := X Z.
+Module M22 : SIG := F Q.
+Module M23 (X: FSIG) : SIG := X Q.
+Module M24 (X Y: FSIG) : SIG := X Q.
+Module M25 (X: FSIG) (Y: SIG) : SIG := X Y.
+Module M26 (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z.
+Module M27 (X: FSIG) (Y: SIG) : SIG := X Y.
+Module M28 (X Y: FSIG) (Z1 Z: SIG) : SIG := X Z.
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index f5f5a9d1..89f11059 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -17,10 +17,12 @@ Check (nat |= nat --> nat).
 (* Check that first non empty definition at an empty level can be of any
    associativity *)
 
-Definition marker := O.
+Module Type v1.
 Notation "x +1" := (S x) (at level 8, left associativity).
-Reset marker.
+End v1.
+Module Type v2.
 Notation "x +1" := (S x) (at level 8, right associativity).
+End v2.
 
 (* Check that empty levels (here 8 and 2 in pattern) are added in the
    right order *)
@@ -86,3 +88,11 @@ Notation "'FOO' x" := (S x) (at level 40).
 Goal (2 ++++ 3) = 5.
 reflexivity.
 Abort.
+
+(* Check correct failure handling when a non-constructor notation is
+   used in cases pattern (bug #2724 in 8.3 and 8.4beta) *)
+
+Notation "'FORALL'  x .. y , P" := (forall x, .. (forall y, P) ..)
+  (at level 200, x binder, y binder, right associativity) : type_scope.
+
+Fail Check fun x => match x with S (FORALL x, _) => 0 end.
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 2602c7e3..64048fe2 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -1,3 +1,5 @@
+Module Type LocalNat.
+
 Inductive nat : Set :=
  | O : nat
  | S : nat->nat.
@@ -5,7 +7,8 @@ Check nat.
 Check O.
 Check S.
 
-Reset nat.
+End LocalNat.
+
 Print nat.
 
 
@@ -477,10 +480,10 @@ Qed.
 
 
 
-(*
 
-Check (fun (P:Prop->Prop)(p: ex_Prop P) =>
+Fail Check (fun (P:Prop->Prop)(p: ex_Prop P) =>
       match p with exP_intro X HX => X end).
+(*
 Error:
 Incorrect elimination of "p" in the inductive type
 "ex_Prop", the return type has sort "Type" while it should be
@@ -489,12 +492,11 @@ Incorrect elimination of "p" in the inductive type
 Elimination of an inductive object of sort "Prop"
 is not allowed on a predicate in sort "Type"
 because proofs can be eliminated only to build proofs
-
 *)
 
-(*
-Check (match prop_inject with (prop_intro P p) => P end).
 
+Fail Check (match prop_inject with (prop_intro p) => p end).
+(*
 Error:
 Incorrect elimination of "prop_inject" in the inductive type
 "prop", the return type has sort "Type" while it should be
@@ -503,13 +505,12 @@ Incorrect elimination of "prop_inject" in the inductive type
 Elimination of an inductive object of sort "Prop"
 is not allowed on a predicate in sort "Type"
 because proofs can be eliminated only to build proofs
-
 *)
 Print prop_inject.
 
 (*
 prop_inject =
-prop_inject = prop_intro prop (fun H : prop => H)
+prop_inject = prop_intro prop
      : prop
 *)
 
@@ -520,26 +521,24 @@ Inductive  typ : Type :=
 Definition typ_inject: typ.
 split.
 exact typ.
+Fail Defined.
 (*
-Defined.
-
 Error: Universe Inconsistency.
 *)
 Abort.
-(*
 
-Inductive aSet : Set :=
+Fail Inductive aSet : Set :=
   aSet_intro: Set -> aSet.
-
-
+(*
 User error: Large non-propositional inductive types must be in Type
-
 *)
 
 Inductive ex_Set  (P : Set -> Prop) : Type :=
   exS_intro : forall X : Set, P X -> ex_Set P.
 
 
+Module Type Version1.
+
 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).
 
@@ -553,21 +552,15 @@ Goal ~(comes_from_the_left _ _ (or_intror True I)).
  *)
 Abort.
 
-Reset comes_from_the_left.
-
-(*
+End Version1.
 
-
-
-
-
-
- Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop :=
+Fail Definition comes_from_the_left (P Q:Prop)(H:P \/ Q): Prop :=
   match H with
          |  or_introl p => True
          |  or_intror q => False
   end.
 
+(*
 Error:
 Incorrect elimination of "H" in the inductive type
 "or", the return type has sort "Type" while it should be
@@ -576,7 +569,6 @@ Incorrect elimination of "H" in the inductive type
 Elimination of an inductive object of sort "Prop"
 is not allowed on a predicate in sort "Type"
 because proofs can be eliminated only to build proofs
-
 *)
 
 Definition comes_from_the_left_sumbool
@@ -737,6 +729,7 @@ Fixpoint plus'' (n p:nat) {struct n} : nat :=
           | S m => plus'' m (S p)
  end.
 
+Module Type even_test_v1.
 
 Fixpoint even_test (n:nat) : bool :=
   match n
@@ -745,8 +738,9 @@ Fixpoint even_test (n:nat) : bool :=
      | S (S p) => even_test p
   end.
 
+End even_test_v1.
 
-Reset even_test.
+Module even_test_v2.
 
 Fixpoint even_test (n:nat) : bool :=
   match n
@@ -761,12 +755,8 @@ with odd_test (n:nat) : bool :=
      | S p => even_test p
  end.
 
-
-
 Eval simpl in even_test.
 
-
-
 Eval simpl in (fun x : nat => even_test x).
 
 Eval simpl in (fun x : nat => plus 5 x).
@@ -774,6 +764,8 @@ Eval simpl in (fun x : nat => even_test (plus 5 x)).
 
 Eval simpl in (fun x : nat => even_test (plus x 5)).
 
+End even_test_v2.
+
 
 Section Principle_of_Induction.
 Variable    P               : nat -> Prop.
@@ -866,14 +858,13 @@ Print Acc.
 
 Require Import Minus.
 
-(*
-Fixpoint div (x y:nat){struct x}: nat :=
+Fail Fixpoint div (x y:nat){struct x}: nat :=
  if eq_nat_dec x 0
   then 0
   else if eq_nat_dec y 0
        then x
        else S (div (x-y) y).
-
+(*
 Error:
 Recursive definition of div is ill-formed.
 In environment
@@ -971,19 +962,15 @@ Proof.
  intros A v;inversion v.
 Abort.
 
-(*
- 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 Vector.t0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),                                    n= 0 -> v = Vnil A.
->                                                                                                                 ^^^^^^
+Fail Lemma vector0_is_vnil_aux : forall (A:Set)(n:nat)(v:Vector.t A n),
+                                  n= 0 -> v = Vector.nil A.
+(*
 Error: In environment
 A : Set
 n : nat
 v : Vector.t A n
-e : n = 0
-The term "Vnil A" has type "Vector.t A 0" while it is expected to have type
+The term "[]" has type "Vector.t A 0" while it is expected to have type
  "Vector.t A n"
 *)
  Require Import JMeq.
diff --git a/test-suite/success/Reset.v b/test-suite/success/Reset.v
deleted file mode 100644
index b71ea69d..00000000
--- a/test-suite/success/Reset.v
+++ /dev/null
@@ -1,7 +0,0 @@
-(* Check Reset Section *)
-
-Section A.
-Definition B := Prop.
-End A.
-
-Reset A.
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index e3183ef2..d3c76101 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -97,13 +97,14 @@ Qed.
 
 (* Check use of unification of bindings types in specialize *)
 
+Module Type Test.
 Variable P : nat -> Prop.
 Variable L : forall (l : nat), P l -> P l.
 Goal P 0 -> True.
 intros.
 specialize L with (1:=H).
 Abort.
-Reset P.
+End Test.
 
 (* Two examples that show that hnf_constr is used when unifying types
    of bindings (a simplification of a script from Field_Theory) *)
@@ -415,3 +416,17 @@ apply mapfuncomp.
 Abort.
 
 End A.
+
+(* Check "with" clauses refer to names as they are printed *)
+
+Definition hide p := forall n:nat, p = n.
+
+Goal forall n, (forall n, n=0) -> hide n -> n=0.
+unfold hide.
+intros n H H'.
+(* H is displayed as (forall n, n=0) *)
+apply H with (n:=n).
+Undo.
+(* H' is displayed as (forall n0, n=n0) *)
+apply H' with (n0:=0).
+Qed.
diff --git a/test-suite/success/coercions.v b/test-suite/success/coercions.v
index 001beae7..4292ecb6 100644
--- a/test-suite/success/coercions.v
+++ b/test-suite/success/coercions.v
@@ -89,3 +89,45 @@ Module A.
 End A.
 Import A.
 Fail Check S true.
+
+(* Tests after the inheritance condition constraint is relaxed *)
+
+Inductive list (A : Type) : Type := 
+  nil : list A | cons : A -> list A -> list A.
+Inductive vect (A : Type) : nat -> Type :=
+  vnil : vect A 0 | vcons : forall n, A -> vect A n -> vect A (1+n).
+Fixpoint size A (l : list A) : nat := match l with nil => 0 | cons _ tl => 1+size _ tl end.
+
+Section test_non_unif_but_complete.
+Fixpoint l2v A (l : list A) : vect A (size A l) :=
+  match l as l return vect A (size A l) with
+  | nil => vnil A
+  | cons x xs => vcons A (size A xs) x (l2v A xs)
+  end.
+
+Local Coercion l2v : list >-> vect.
+Check (fun l : list nat =>  (l : vect _ _)).
+
+End test_non_unif_but_complete.
+
+Section what_we_could_do.
+Variables T1 T2 : Type.
+Variable c12 : T1 -> T2.
+
+Class coercion (A B : Type) : Type := cast : A -> B.
+Instance atom : coercion T1 T2 := c12.
+Instance pair A B C D (c1 : coercion A B) (c2 : coercion C D) : coercion (A * C) (B * D) :=
+  fun x => (c1 (fst x), c2 (snd x)).
+
+Fixpoint l2v2 {A B} {c : coercion A B} (l : list A) : (vect B (size A l)) := 
+  match l as l return vect B (size A l) with
+  | nil => vnil B
+  | cons x xs => vcons _ _ (c x) (l2v2 xs) end.
+
+Local Coercion l2v2 : list >-> vect.
+
+(* This shows that there is still something to do to take full profit
+   of coercions *)
+Fail Check (fun l : list (T1 * T1) => (l : vect _ _)).
+Check (fun l : list (T1 * T1) => (l2v2 l : vect _ _)).
+Section what_we_could_do.
\ No newline at end of file
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index fe0165d0..79d12a06 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -1,5 +1,11 @@
 Require Import Coq.Program.Program Coq.Program.Equality.
 
+Goal forall (H: forall n m : nat, n = m -> n = 0) x, x = tt.
+intros.
+dependent destruction x.
+reflexivity.
+Qed.
+
 Variable A : Set.
 
 Inductive vector : nat -> Type := vnil : vector 0 | vcons : A -> forall {n}, vector n -> vector (S n).
@@ -84,6 +90,29 @@ Proof with simpl in * ; eqns ; eauto with lambda.
   intro. eapply app...
 Defined.
 
+Lemma weakening_ctx : forall Γ Δ τ, Γ ; Δ ⊢ τ ->
+  forall Δ', Γ ; Δ' ; Δ ⊢ τ.
+Proof with simpl in * ; eqns ; eauto with lambda.
+  intros Γ Δ τ H.
+
+  dependent induction H.
+
+  destruct Δ as [|Δ τ'']...
+  induction Δ'...
+
+  destruct Δ as [|Δ τ'']...
+  induction Δ'...
+
+  destruct Δ as [|Δ τ'']...
+    apply abs.
+    specialize (IHterm Γ (empty, τ))...
+
+    apply abs.
+    specialize (IHterm Γ (Δ, τ'', τ))...
+
+  intro. eapply app...
+Defined.
+
 Lemma exchange : forall Γ Δ α β τ, term (Γ, α, β ; Δ) τ -> term (Γ, β, α ; Δ) τ.
 Proof with simpl in * ; eqns ; eauto.
   intros until 1.
@@ -105,6 +134,8 @@ Proof with simpl in * ; eqns ; eauto.
   eapply app...
 Defined.
 
+
+
 (** Example by Andrew Kenedy, uses simplification of the first component of dependent pairs. *)
 
 Set Implicit Arguments.
diff --git a/test-suite/success/evars.v b/test-suite/success/evars.v
index 2f1ec757..e6088091 100644
--- a/test-suite/success/evars.v
+++ b/test-suite/success/evars.v
@@ -309,3 +309,73 @@ Definition k6
 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).
+
+(* An example that uses materialize_evar under binders *)
+(* Extracted from bigop.v in the mathematical components library *)
+
+Section Bigop.
+
+Variable bigop : forall R I: Type,
+  R -> (R -> R -> R) -> list I -> (I->Prop) -> (I -> R) -> R.
+
+Hypothesis eq_bigr :
+forall (R : Type) (idx : R) (op : R -> R -> R)
+       (I : Type) (r : list I) (P : I -> Prop) (F1 F2 : I -> R),
+       (forall i : I, P i -> F1 i = F2 i) ->
+       bigop R I idx op r (fun i : I => P i) (fun i : I => F1 i) = idx.
+
+Hypothesis big_tnth :
+forall (R : Type) (idx : R) (op : R -> R -> R)
+     (I : Type) (r : list I) (P : I -> Prop) (F : I -> R),
+     bigop R I idx op r (fun i : I => P i) (fun i : I => F i) = idx.
+
+Hypothesis big_tnth_with_letin :
+forall (R : Type) (idx : R) (op : R -> R -> R)
+     (I : Type) (r : list I) (P : I -> Prop) (F : I -> R),
+     bigop R I idx op r (fun i : I => let i:=i in P i) (fun i : I => F i) = idx.
+
+Variable R : Type.
+Variable idx : R.
+Variable op : R -> R -> R.
+Variable I : Type.
+Variable J : Type.
+Variable rI : list I.
+Variable rJ : list J.
+Variable xQ : J -> Prop.
+Variable P : I -> Prop.
+Variable Q : I -> J -> Prop.
+Variable F : I -> J -> R.
+
+(* Check unification under binders *)
+
+Check (eq_bigr _ _ _ _ _ _ _ _ (fun _ _ => big_tnth _ _ _ _ rI _ _))
+  : (bigop R J idx op rJ
+        (fun j : J => let k:=j in xQ k)
+        (fun j : J => let k:=j in 
+         bigop R I idx
+           op rI
+           (fun i : I => P i /\ Q i k) (fun i : I => let k:=j in F i k))) = idx.
+
+(* Check also with let-in *)
+
+Check (eq_bigr _ _ _ _ _ _ _ _ (fun _ _ => big_tnth_with_letin _ _ _ _ rI _ _))
+  : (bigop R J idx op rJ
+        (fun j : J => let k:=j in xQ k)
+        (fun j : J => let k:=j in 
+         bigop R I idx
+           op rI
+           (fun i : I => P i /\ Q i k) (fun i : I => let k:=j in F i k))) = idx.
+
+End Bigop.
+
+(* Check the use of (at least) an heuristic to solve problems of the form
+   "?x[t] = ?y" where ?y occurs in t without easily knowing if ?y can
+   eventually be erased in t *)
+
+Section evar_evar_occur.
+  Variable id : nat -> nat.
+  Variable f : forall x, id x = 0 -> id x = 0 -> x = 1 /\ x = 2.
+  Variable g : forall y, id y = 0 /\ id y = 0.
+  (* Still evars in the resulting type, but constraints should be solved *)
+  Check match g _ with conj a b => f _ a b end.
+End evar_evar_occur.
diff --git a/test-suite/success/hyps_inclusion.v b/test-suite/success/hyps_inclusion.v
index af81e53d..ebd90a40 100644
--- a/test-suite/success/hyps_inclusion.v
+++ b/test-suite/success/hyps_inclusion.v
@@ -19,14 +19,16 @@ red in H.
 (* next tactic was failing wrt bug #1325 because type-checking the goal
    detected a syntactically different type for the section variable H *)
 case 0.
-Reset A.
+Abort.
+End A.
 
 (* Variant with polymorphic inductive types for bug #1325 *)
 
-Section A.
+Section B.
 Variable H:not True.
 Inductive I (n:nat) : Type := C : H=H -> I n.
 Goal I 0.
 red in H.
 case 0.
-Reset A.
+Abort.
+End B.
diff --git a/test-suite/success/telescope_canonical.v b/test-suite/success/telescope_canonical.v
index 8a607c93..73df5ca9 100644
--- a/test-suite/success/telescope_canonical.v
+++ b/test-suite/success/telescope_canonical.v
@@ -1,12 +1,72 @@
 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.
+Lemma test1 (n : hidden_nat) : P _ n.
 Admitted.
+
+Structure Pnat := mkP { getp : nat }.
+Definition my_getp := getp.
+Axiom W : nat -> Prop.
+
+(* Fix *)
+Canonical Structure add1Pnat n := mkP (plus n 1).
+Definition test_fix n := (refl_equal _ : W (my_getp _)  = W (n + 1)).
+
+(* Case *)
+Definition pred n := match n with 0 => 0 | S m => m end.
+Canonical Structure predSS n := mkP (pred n).
+Definition test_case x := (refl_equal _ : W (my_getp _)  = W (pred x)).
+Fail Definition test_case' := (refl_equal _ : W (my_getp _)  = W (pred 0)).
+
+Canonical Structure letPnat' := mkP 0.
+Definition letin := (let n := 0 in n).
+Definition test4 := (refl_equal _ : W (getp _)  = W letin).
+Definition test41 := (refl_equal _ : W (my_getp _)  = W letin).
+Definition letin2 (x : nat) := (let n := x in n).
+Canonical Structure letPnat'' x := mkP (letin2 x).
+Definition test42 x := (refl_equal _ : W (my_getp _)  = W (letin2 x)).
+Fail Definition test42' x := (refl_equal _ : W (my_getp _)  = W x).
+
+Structure Morph := mkM { f :> nat -> nat }.
+Definition my_f := f.
+Axiom Q : (nat -> nat) -> Prop.
+
+(* Lambda *)
+Canonical Structure addMorh x := mkM (plus x).
+Definition test_lam x := (refl_equal _ : Q (my_f _) = Q (plus x)).
+Definition test_lam' := (refl_equal _ : Q (my_f _) = Q (plus 0)).
+
+(* Simple tests to justify Sort and Prod as "named". 
+   They are already normal, so they cannot loose their names, 
+   but still... *)
+Structure Sot := mkS { T : Type }.
+Axiom R : Type -> Prop.
+Canonical Structure tsot := mkS (Type).
+Definition test_sort := (refl_equal _ : R (T _) = R Type).
+Canonical Structure tsot2 := mkS (nat -> nat).
+Definition test_prod := (refl_equal _ : R (T _) = R (nat -> nat)).
+
+(* Var *)
+Section Foo.
+Variable v : nat.
+Definition my_v := v.
+Canonical Structure vP := mkP my_v.
+Definition test_var := (refl_equal _ : W (getp _)  = W my_v).
+Canonical Structure vP' := mkP v.
+Definition test_var' := (refl_equal _ : W (my_getp _)  = W my_v).
+End Foo.
+
+(* Rel *)
+Definition test_rel v := (refl_equal _ : W (my_getp _)  = W (my_v v)).
+Goal True.
+pose (x := test_rel 2).
+match goal with x := _ : W (my_getp (vP 2)) = _ |- _ => idtac end.
+apply I.
+Qed.
+
+
+
+