Imported Upstream version 8.4dfsgupstream/8.4dfsg

71 files changed, 296 insertions, 210 deletions

diff --git a/test-suite/bench/lists-100.v b/test-suite/bench/lists-100.v
index 3d145d96..f9821f76 100644
--- a/test-suite/bench/lists-100.v
+++ b/test-suite/bench/lists-100.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/bench/lists_100.v b/test-suite/bench/lists_100.v
index 3d145d96..f9821f76 100644
--- a/test-suite/bench/lists_100.v
+++ b/test-suite/bench/lists_100.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/bugs/closed/shouldsucceed/1414.v b/test-suite/bugs/closed/shouldsucceed/1414.v
index 495a16bc..ee9e2504 100644
--- a/test-suite/bugs/closed/shouldsucceed/1414.v
+++ b/test-suite/bugs/closed/shouldsucceed/1414.v
@@ -26,13 +26,13 @@ Program Fixpoint union
     | t1,Leaf => t1
     | Node l1 v1 r1 h1, Node l2 v2 r2 h2 =>
         if (Z_ge_lt_dec h1 h2) then
-          if (Z_eq_dec h2 1)
+          if (Z.eq_dec h2 1)
           then add v2 s
           else
             let (l2', r2') := split v1 u in
             join (union l1 l2' _ _ _ _) v1 (union r1 (snd r2') _ _ _ _)
         else
-          if (Z_eq_dec h1 1)
+          if (Z.eq_dec h1 1)
           then add v1 s
           else
             let (l1', r1') := split v2 u in
diff --git a/test-suite/bugs/closed/shouldsucceed/1784.v b/test-suite/bugs/closed/shouldsucceed/1784.v
index 718b0e86..fb2f0ca9 100644
--- a/test-suite/bugs/closed/shouldsucceed/1784.v
+++ b/test-suite/bugs/closed/shouldsucceed/1784.v
@@ -58,7 +58,7 @@ Program Fixpoint lt_dec (x y:sv) { struct x } : {slt x y}+{~slt x y} :=
   match x with
     | I x =>
       match y with
-        | I y => if (Z_eq_dec x y) then in_left else in_right
+        | I y => if (Z.eq_dec x y) then in_left else in_right
         | S ys => in_right
       end
     | S xs =>
diff --git a/test-suite/bugs/closed/shouldsucceed/1844.v b/test-suite/bugs/closed/shouldsucceed/1844.v
index 5627612f..17eeb352 100644
--- a/test-suite/bugs/closed/shouldsucceed/1844.v
+++ b/test-suite/bugs/closed/shouldsucceed/1844.v
@@ -1,6 +1,6 @@
 Require Import ZArith.
 
-Definition zeq := Z_eq_dec.
+Definition zeq := Z.eq_dec.
 
 Definition update (A: Set) (x: Z) (v: A) (s: Z -> A) : Z -> A :=
  fun y => if zeq x y then v else s y.
diff --git a/test-suite/bugs/closed/shouldsucceed/1935.v b/test-suite/bugs/closed/shouldsucceed/1935.v
index 72396d49..d5837619 100644
--- a/test-suite/bugs/closed/shouldsucceed/1935.v
+++ b/test-suite/bugs/closed/shouldsucceed/1935.v
@@ -13,7 +13,7 @@ Qed.
 
 Require Import ZArith.
 
-Definition f'' (a:bool) := if a then eq (A:= Z) else Zlt.
+Definition f'' (a:bool) := if a then eq (A:= Z) else Z.lt.
 
 Lemma f_refl'' : forall n , f'' true n n.
 Proof.
diff --git a/test-suite/bugs/closed/shouldsucceed/2127.v b/test-suite/bugs/closed/shouldsucceed/2127.v
index 0fc854b6..142ada26 100644
--- a/test-suite/bugs/closed/shouldsucceed/2127.v
+++ b/test-suite/bugs/closed/shouldsucceed/2127.v
@@ -1,8 +1,8 @@
-(* Check that "apply refl_equal" is not exported as an interactive
+(* Check that "apply eq_refl" is not exported as an interactive
    tactic but as a statically globalized one *)
 
 (* (this is a simplification of the original bug report) *)
 
 Module A.
-Hint Rewrite sym_equal using apply refl_equal : foo.
+Hint Rewrite eq_sym using apply eq_refl : foo.
 End A.
diff --git a/test-suite/bugs/closed/shouldsucceed/2817.v b/test-suite/bugs/closed/shouldsucceed/2817.v
new file mode 100644
index 00000000..08dff992
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2817.v
@@ -0,0 +1,9 @@
+(** Occur-check for Meta (up to application of already known instances) *)
+
+Goal forall (f: nat -> nat -> Prop) (x:bool)
+  (H: forall  (u: nat), f u u -> True)
+  (H0: forall x0, f (if x then x0 else x0) x0),
+False.
+
+intros.
+Fail apply H in H0. (* should fail without exhausting the stack *)
diff --git a/test-suite/bugs/closed/shouldsucceed/2836.v b/test-suite/bugs/closed/shouldsucceed/2836.v
new file mode 100644
index 00000000..a948b75e
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/2836.v
@@ -0,0 +1,39 @@
+(* Check that possible instantiation made during evar materialization
+   are taken into account and do not raise Not_found *)
+
+Set Implicit Arguments.
+
+Record SpecializedCategory (obj : Type) (Morphism : obj -> obj -> Type) := {
+  Object :> _ := obj;
+
+  Identity' : forall o, Morphism o o;
+  Compose' : forall s d d', Morphism d d' -> Morphism s d -> Morphism s d'
+}.
+
+Section SpecializedCategoryInterface.
+  Variable obj : Type.
+  Variable mor : obj -> obj -> Type.
+  Variable C : @SpecializedCategory obj mor.
+
+  Definition Morphism (s d : C) := mor s d.
+  Definition Identity (o : C) : Morphism o o := C.(Identity') o.
+  Definition Compose (s d d' : C) (m : Morphism d d') (m0 : Morphism s d) :
+Morphism s d' := C.(Compose') s d d' m m0.
+End SpecializedCategoryInterface.
+
+Section ProductCategory.
+  Variable objC : Type.
+  Variable morC : objC -> objC -> Type.
+  Variable objD : Type.
+  Variable morD : objD -> objD -> Type.
+  Variable C : SpecializedCategory morC.
+  Variable D : SpecializedCategory morD.
+
+(* Should fail nicely *)
+Definition ProductCategory : @SpecializedCategory (objC * objD)%type (fun s d
+=> (morC (fst s) (fst d) * morD (snd s) (snd d))%type).
+Fail refine {|
+      Identity' := (fun o => (Identity (fst o), Identity (snd o)));
+      Compose' := (fun s d d' m2 m1 => (Compose (fst m2) (fst m1), Compose (snd
+m2) (snd m1)))
+    |}.
diff --git a/test-suite/complexity/ring2.v b/test-suite/complexity/ring2.v
index 6945edc8..52dae265 100644
--- a/test-suite/complexity/ring2.v
+++ b/test-suite/complexity/ring2.v
@@ -3,7 +3,7 @@
 
 Require Import BinInt Zbool.
 
-Definition Zplus x y :=
+Definition Zadd x y :=
 match x with
 | 0%Z => y
 | Zpos x' =>
@@ -30,9 +30,10 @@ match x with
     end
 end.
 
+
 Require Import Ring.
 
-Lemma Zth : ring_theory Z0 (Zpos xH) Zplus Zmult Zminus Zopp (@eq Z).
+Lemma Zth : ring_theory Z0 (Zpos xH) Zadd Z.mul Z.sub Z.opp (@eq Z).
 Admitted.
 
 Ltac Zcst t :=
@@ -45,7 +46,7 @@ Add Ring Zr : Zth
   (decidable Zeq_bool_eq, constants [Zcst]).
 
 Open Scope Z_scope.
-Infix "+" := Zplus : Z_scope.
+Infix "+" := Zadd : Z_scope.
 
 Goal forall a, a+a+a+a+a+a+a+a+a+a+a+a+a = a*13.
 Timeout 5 Time intro; ring.
diff --git a/test-suite/failure/Tauto.v b/test-suite/failure/Tauto.v
index a08c5154..cbe7473c 100644
--- a/test-suite/failure/Tauto.v
+++ b/test-suite/failure/Tauto.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/Uminus.v b/test-suite/failure/Uminus.v
index 6866f19a..3c3bf375 100644
--- a/test-suite/failure/Uminus.v
+++ b/test-suite/failure/Uminus.v
@@ -31,7 +31,7 @@ Lemma Omega : forall i:U -> prop, induct i -> up (i WF).
 Proof.
 intros i y.
 apply y.
-unfold le, WF, induct in |- *.
+unfold le, WF, induct.
 intros x H0.
 apply y.
 exact H0.
@@ -39,7 +39,7 @@ Qed.
 
 Lemma lemma1 : induct (fun u => down (I u)).
 Proof.
-unfold induct in |- *.
+unfold induct.
 intros x p.
 intro q.
 apply (q (fun u => down (I u)) p).
diff --git a/test-suite/failure/clash_cons.v b/test-suite/failure/clash_cons.v
index d000f965..25d3c165 100644
--- a/test-suite/failure/clash_cons.v
+++ b/test-suite/failure/clash_cons.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/fixpoint1.v b/test-suite/failure/fixpoint1.v
index e38fa6e0..6abf6332 100644
--- a/test-suite/failure/fixpoint1.v
+++ b/test-suite/failure/fixpoint1.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/guard.v b/test-suite/failure/guard.v
index 079ad33f..324dc603 100644
--- a/test-suite/failure/guard.v
+++ b/test-suite/failure/guard.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/illtype1.v b/test-suite/failure/illtype1.v
index 64537877..6c14c2c3 100644
--- a/test-suite/failure/illtype1.v
+++ b/test-suite/failure/illtype1.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/pattern.v b/test-suite/failure/pattern.v
index 129c380e..a24beaa2 100644
--- a/test-suite/failure/pattern.v
+++ b/test-suite/failure/pattern.v
@@ -6,4 +6,4 @@ Variable P : forall m : nat, m = n -> Prop.
 
 Goal forall p : n = n, P n p.
 intro.
-pattern n, p in |- *.
+pattern n, p.
diff --git a/test-suite/failure/positivity.v b/test-suite/failure/positivity.v
index e9fbe969..03cc1109 100644
--- a/test-suite/failure/positivity.v
+++ b/test-suite/failure/positivity.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/redef.v b/test-suite/failure/redef.v
index 2b648c13..0c39b276 100644
--- a/test-suite/failure/redef.v
+++ b/test-suite/failure/redef.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/search.v b/test-suite/failure/search.v
index 0ff554d9..38a62766 100644
--- a/test-suite/failure/search.v
+++ b/test-suite/failure/search.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/failure/subtyping2.v b/test-suite/failure/subtyping2.v
index addd3b45..48fc2fff 100644
--- a/test-suite/failure/subtyping2.v
+++ b/test-suite/failure/subtyping2.v
@@ -54,7 +54,7 @@ Section Inverse_Image.
     Qed.
 
   Lemma WF_inverse_image : WF B R -> WF A Rof.
-    red in |- *; intros; apply ACC_inverse_image; auto.
+    red; intros; apply ACC_inverse_image; auto.
     Qed.
 
 End Inverse_Image.
@@ -104,7 +104,7 @@ generalize eqx0; clear eqx0.
 elim eqy using eq_ind_r; intro.
 case (inj _ _ _ _ eqx0); intros.
 exists X1 R1 X3 R3 (fun x : X1 => f0 (x0 (f x))) maj0; trivial.
-red in |- *; auto.
+red; auto.
 Defined.
 
 
@@ -122,7 +122,7 @@ apply sym_eq; assumption.
 
 intros.
 apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
- try red in |- *; auto.
+ try red; auto.
 Defined.
 
   (* The embedding relation is well founded *)
@@ -158,7 +158,7 @@ Section Subsets.
 exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
 exact WF_emb.
 
-red in |- *; trivial.
+red; trivial.
 
 exact emb_wit.
 Defined.
@@ -174,7 +174,7 @@ End Subsets.
       - the upper bound is a, which is in F(b) since a < b
    *)
   Lemma F_morphism : morphism A0 emb A0 emb F.
-red in |- *; intros.
+red; intros.
 exists
  (sub x)
    (Rof _ _ emb (witness x))
@@ -185,10 +185,10 @@ exists
 apply WF_inverse_image.
 exact WF_emb.
 
-unfold morphism, Rof, fsub in |- *; simpl in |- *; intros.
+unfold morphism, Rof, fsub; simpl; intros.
 trivial.
 
-unfold Rof, fsub in |- *; simpl in |- *; intros.
+unfold Rof, fsub; simpl; intros.
 apply emb_wit.
 Defined.
 
@@ -230,10 +230,10 @@ intros.
 change
   match i0' X1 R1, i0' X2 R2 with
   | i0 x1 r1, i0 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
-  end in |- *.
-case H; simpl in |- *.
+  end.
+case H; simpl.
 exists (fun x : X1 => x).
-red in |- *; trivial.
+red; trivial.
 Defined.
 
 (* The following command raises 'Error: Universe Inconsistency'.
diff --git a/test-suite/failure/universes-buraliforti-redef.v b/test-suite/failure/universes-buraliforti-redef.v
index 034b7f09..a8b5b975 100644
--- a/test-suite/failure/universes-buraliforti-redef.v
+++ b/test-suite/failure/universes-buraliforti-redef.v
@@ -54,7 +54,7 @@ Section Inverse_Image.
     Qed.
 
   Lemma WF_inverse_image : WF B R -> WF A Rof.
-    red in |- *; intros; apply ACC_inverse_image; auto.
+    red; intros; apply ACC_inverse_image; auto.
     Qed.
 
 End Inverse_Image.
@@ -106,7 +106,7 @@ generalize eqx0; clear eqx0.
 elim eqy using eq_ind_r; intro.
 case (inj _ _ _ _ eqx0); intros.
 exists X1 R1 X4 R4 (fun x : X1 => f0 (x0 (f x))) maj0; trivial.
-red in |- *; auto.
+red; auto.
 Defined.
 
 
@@ -124,7 +124,7 @@ apply sym_eq; assumption.
 
 intros.
 apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
- try red in |- *; auto.
+ try red; auto.
 Defined.
 
   (* The embedding relation is well founded *)
@@ -160,7 +160,7 @@ Section Subsets.
 exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
 exact WF_emb.
 
-red in |- *; trivial.
+red; trivial.
 
 exact emb_wit.
 Defined.
@@ -176,7 +176,7 @@ End Subsets.
       - the upper bound is a, which is in F(b) since a < b
    *)
   Lemma F_morphism : morphism A0 emb A0 emb F.
-red in |- *; intros.
+red; intros.
 exists
  (sub x)
    (Rof _ _ emb (witness x))
@@ -187,10 +187,10 @@ exists
 apply WF_inverse_image.
 exact WF_emb.
 
-unfold morphism, Rof, fsub in |- *; simpl in |- *; intros.
+unfold morphism, Rof, fsub; simpl; intros.
 trivial.
 
-unfold Rof, fsub in |- *; simpl in |- *; intros.
+unfold Rof, fsub; simpl; intros.
 apply emb_wit.
 Defined.
 
@@ -231,10 +231,10 @@ intros.
 change
   match i0 X1 R1, i0 X2 R2 with
   | i1 x1 r1, i1 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
-  end in |- *.
-case H; simpl in |- *.
+  end.
+case H; simpl.
 exists (fun x : X1 => x).
-red in |- *; trivial.
+red; trivial.
 Defined.
 
 (* The following command raises 'Error: Universe Inconsistency'.
diff --git a/test-suite/failure/universes-buraliforti.v b/test-suite/failure/universes-buraliforti.v
index 1f96ab34..7b62a0c5 100644
--- a/test-suite/failure/universes-buraliforti.v
+++ b/test-suite/failure/universes-buraliforti.v
@@ -37,7 +37,7 @@ Section Inverse_Image.
     Qed.
 
   Lemma WF_inverse_image : WF B R -> WF A Rof.
-    red in |- *; intros; apply ACC_inverse_image; auto.
+    red; intros; apply ACC_inverse_image; auto.
     Qed.
 
 End Inverse_Image.
@@ -90,7 +90,7 @@ generalize eqx0; clear eqx0.
 elim eqy using eq_ind_r; intro.
 case (inj _ _ _ _ eqx0); intros.
 exists X1 R1 X3 R3 (fun x : X1 => f0 (x0 (f x))) maj0; trivial.
-red in |- *; auto.
+red; auto.
 Defined.
 
 
@@ -108,7 +108,7 @@ apply sym_eq; assumption.
 
 intros.
 apply H1 with (y := f (x1 maj)) (f := fun x : X1 => f (x1 (f0 x)));
- try red in |- *; auto.
+ try red; auto.
 Defined.
 
   (* The embedding relation is well founded *)
@@ -144,7 +144,7 @@ Section Subsets.
 exists sub (Rof _ _ emb witness) A0 emb witness a; trivial.
 exact WF_emb.
 
-red in |- *; trivial.
+red; trivial.
 
 exact emb_wit.
 Defined.
@@ -160,7 +160,7 @@ End Subsets.
       - the upper bound is a, which is in F(b) since a < b
    *)
   Lemma F_morphism : morphism A0 emb A0 emb F.
-red in |- *; intros.
+red; intros.
 exists
  (sub x)
    (Rof _ _ emb (witness x))
@@ -171,10 +171,10 @@ exists
 apply WF_inverse_image.
 exact WF_emb.
 
-unfold morphism, Rof, fsub in |- *; simpl in |- *; intros.
+unfold morphism, Rof, fsub; simpl; intros.
 trivial.
 
-unfold Rof, fsub in |- *; simpl in |- *; intros.
+unfold Rof, fsub; simpl; intros.
 apply emb_wit.
 Defined.
 
@@ -222,10 +222,10 @@ intros.
 change
   match i0 X1 R1, i0 X2 R2 with
   | i0 x1 r1, i0 x2 r2 => exists f : _, morphism x1 r1 x2 r2 f
-  end in |- *.
-case H; simpl in |- *.
+  end.
+case H; simpl.
 exists (fun x : X1 => x).
-red in |- *; trivial.
+red; trivial.
 Defined.
 
 (* The following command raises 'Error: Universe Inconsistency'.
diff --git a/test-suite/ideal-features/Apply.v b/test-suite/ideal-features/Apply.v
index 8b36f44b..7628b961 100644
--- a/test-suite/ideal-features/Apply.v
+++ b/test-suite/ideal-features/Apply.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/ideal-features/eapply_evar.v b/test-suite/ideal-features/eapply_evar.v
index 547860bf..bb61afb8 100644
--- a/test-suite/ideal-features/eapply_evar.v
+++ b/test-suite/ideal-features/eapply_evar.v
@@ -4,6 +4,6 @@
    and not "O = O" *)
 
 Lemma eapply_evar : O=O -> 0=O.
-intro H; eapply trans_equal;
+intro H; eapply eq_trans;
   [apply H | match goal with |- ?x = ?x => reflexivity end].
 Qed.
diff --git a/test-suite/micromega/example.v b/test-suite/micromega/example.v
index f424f0fc..d648c2e4 100644
--- a/test-suite/micromega/example.v
+++ b/test-suite/micromega/example.v
@@ -77,13 +77,13 @@ Definition rbound2 (C:Z -> Z -> Z) : Prop :=
 
 Lemma bounded_drift : forall s t p q C D, s <= t /\ correct p t  /\ correct q t /\
   rbound1 C /\ rbound2 C /\ rbound1 D /\ rbound2 D  ->
-  Zabs (C p t - D q t) <= Zabs (C p s - D q s) + 2 * rho * (t- s).
+  Z.abs (C p t - D q t) <= Z.abs (C p s - D q s) + 2 * rho * (t- s).
 Proof.
   intros.
-  generalize (Zabs_eq (C p t - D q t)).
-  generalize (Zabs_non_eq (C p t - D q t)).
-  generalize (Zabs_eq (C p s -D q s)).
-  generalize (Zabs_non_eq (C p s - D q s)).
+  generalize (Z.abs_eq (C p t - D q t)).
+  generalize (Z.abs_neq (C p t - D q t)).
+  generalize (Z.abs_eq (C p s -D q s)).
+  generalize (Z.abs_neq (C p s - D q s)).
   unfold rbound2 in H.
   unfold rbound1 in H.
   intuition.
diff --git a/test-suite/micromega/square.v b/test-suite/micromega/square.v
index 4c00ffe4..8767f687 100644
--- a/test-suite/micromega/square.v
+++ b/test-suite/micromega/square.v
@@ -9,17 +9,17 @@
 Require Import ZArith Zwf Psatz QArith.
 Open Scope Z_scope.
 
-Lemma Zabs_square : forall x,  (Zabs  x)^2 = x^2.
+Lemma Zabs_square : forall x,  (Z.abs  x)^2 = x^2.
 Proof.
  intros ; case (Zabs_dec x) ; intros ; psatz Z 2.
 Qed.
-Hint Resolve Zabs_pos Zabs_square.
+Hint Resolve Z.abs_nonneg Zabs_square.
 
 Lemma integer_statement :  ~exists n, exists p, n^2 = 2*p^2 /\ n <> 0.
 Proof.
-intros [n [p [Heq Hnz]]]; pose (n' := Zabs n); pose (p':=Zabs p).
-assert (facts : 0 <= Zabs n /\ 0 <= Zabs p /\ Zabs n^2=n^2
-         /\ Zabs p^2 = p^2) by auto.
+intros [n [p [Heq Hnz]]]; pose (n' := Z.abs n); pose (p':=Z.abs p).
+assert (facts : 0 <= Z.abs n /\ 0 <= Z.abs p /\ Z.abs n^2=n^2
+         /\ Z.abs p^2 = p^2) by auto.
 assert (H : (0 < n' /\ 0 <= p' /\ n' ^2 = 2* p' ^2)) by
   (destruct facts as [Hf1 [Hf2 [Hf3 Hf4]]]; unfold n', p' ; psatz Z 2).
 generalize p' H; elim n' using (well_founded_ind (Zwf_well_founded 0)); clear.
@@ -35,7 +35,7 @@ Lemma QnumZpower : forall x : Q, Qnum (x ^ 2)%Q = ((Qnum x) ^ 2) %Z.
 Proof.
   intros.
   destruct x.
-  cbv beta  iota zeta delta - [Zmult].
+  cbv beta  iota zeta delta - [Z.mul].
   ring.
 Qed.
 
@@ -45,15 +45,15 @@ Proof.
   intros.
   destruct x.
   simpl.
-  unfold Zpower_pos.
+  unfold Z.pow_pos.
   simpl.
-  rewrite Pmult_1_r.
+  rewrite Pos.mul_1_r.
   reflexivity.
 Qed.
 
 Theorem sqrt2_not_rational : ~exists x:Q, x^2==2#1.
 Proof.
- unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Zmult_1_r.
+ unfold Qeq; intros [x]; simpl (Qden (2#1)); rewrite Z.mul_1_r.
  intros HQeq.
  assert (Heq : (Qnum x ^ 2 = 2 * ' Qden x ^ 2%Q)%Z) by
    (rewrite QnumZpower in HQeq ; rewrite QdenZpower in HQeq ; auto).
diff --git a/test-suite/misc/berardi_test.v b/test-suite/misc/berardi_test.v
index 2b388687..38377573 100644
--- a/test-suite/misc/berardi_test.v
+++ b/test-suite/misc/berardi_test.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -45,7 +45,7 @@ Lemma AC_IF :
    (B -> Q e1) -> (~ B -> Q e2) -> Q (IFProp B e1 e2).
 Proof.
 intros P B e1 e2 Q p1 p2.
-unfold IFProp in |- *.
+unfold IFProp.
 case (EM B); assumption.
 Qed.
 
@@ -76,7 +76,7 @@ Record retract_cond : Prop :=
 Lemma AC : forall r:retract_cond, retract -> forall a:A, j2 r (i2 r a) = a.
 Proof.
 intros r.
-case r; simpl in |- *.
+case r; simpl.
 trivial.
 Qed.
 
@@ -113,7 +113,7 @@ Lemma retract_pow_U_U : retract (pow U) U.
 Proof.
 exists g f.
 intro a.
-unfold f, g in |- *; simpl in |- *.
+unfold f, g; simpl.
 apply AC.
 exists (fun x:pow U => x) (fun x:pow U => x).
 trivial.
@@ -130,8 +130,8 @@ Definition R : U := g (fun u:U => Not_b (u U u)).
 
 Lemma not_has_fixpoint : R R = Not_b (R R).
 Proof.
-unfold R at 1 in |- *.
-unfold g in |- *.
+unfold R at 1.
+unfold g.
 rewrite AC with (r := L1 U U) (a := fun u:U => Not_b (u U u)).
 trivial.
 exists (fun x:pow U => x) (fun x:pow U => x); trivial.
@@ -141,7 +141,7 @@ Qed.
 Theorem classical_proof_irrelevence : T = F.
 Proof.
 generalize not_has_fixpoint.
-unfold Not_b in |- *.
+unfold Not_b.
 apply AC_IF.
 intros is_true is_false.
 elim is_true; elim is_false; trivial.
diff --git a/test-suite/modules/PO.v b/test-suite/modules/PO.v
index 71d33177..6198f29a 100644
--- a/test-suite/modules/PO.v
+++ b/test-suite/modules/PO.v
@@ -27,13 +27,13 @@ Module Pair (X: PO) (Y: PO) <: PO.
   Qed.
 
   Lemma le_trans : forall p1 p2 p3 : T, le p1 p2 -> le p2 p3 -> le p1 p3.
-    unfold le in |- *;  intuition; info  eauto.
+    unfold le;  intuition; info  eauto.
   Qed.
 
   Lemma le_antis : forall p1 p2 : T, le p1 p2 -> le p2 p1 -> p1 = p2.
     destruct p1.
     destruct p2.
-    unfold le in |- *.
+    unfold le.
      intuition.
      cutrewrite (t = t1).
      cutrewrite (t0 = t2).
diff --git a/test-suite/modules/Przyklad.v b/test-suite/modules/Przyklad.v
index e3694b81..341805a1 100644
--- a/test-suite/modules/Przyklad.v
+++ b/test-suite/modules/Przyklad.v
@@ -66,7 +66,7 @@ Module FuncDict (E: ELEM).
   Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true.
 
     intros.
-    unfold find, add in |- *.
+    unfold find, add.
     elim (Reflexivity_provable _ _ (E.eq_dec e e)).
     intros.
      rewrite H.
@@ -77,13 +77,13 @@ Module FuncDict (E: ELEM).
   Lemma find_add_false :
    forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s.
     intros.
-    unfold add, find in |- *.
+    unfold add, find.
     cut (exists x : _, E.eq_dec e' e = right _ x).
     intros.
     elim H0.
     intros.
      rewrite H1.
-    unfold ifte in |- *.
+    unfold ifte.
     reflexivity.
 
     apply Disequality_provable.
@@ -123,7 +123,7 @@ Module Lemmas (G: SET) (E: ELEM).
    forall a : E.T, ESet.find a S1 = ESet.find a S2.
 
     intros.
-    unfold S1, S2 in |- *.
+    unfold S1, S2.
     elim (E.eq_dec a a1); elim (E.eq_dec a a2); intros H1 H2;
      try  rewrite <- H1; try  rewrite <- H2;
      repeat
@@ -153,7 +153,7 @@ Module ListDict (E: ELEM).
 
   Lemma find_add_true : forall (s : T) (e : E.T), find e (add e s) = true.
     intros.
-    simpl in |- *.
+    simpl.
     elim (Reflexivity_provable _ _ (E.eq_dec e e)).
     intros.
      rewrite H.
@@ -165,11 +165,11 @@ Module ListDict (E: ELEM).
   Lemma find_add_false :
    forall (s : T) (e e' : E.T), e <> e' -> find e (add e' s) = find e s.
     intros.
-    simpl in |- *.
+    simpl.
     elim (Disequality_provable _ _ _ H (E.eq_dec e e')).
     intros.
      rewrite H0.
-    simpl in |- *.
+    simpl.
     reflexivity.
   Qed.
 
diff --git a/test-suite/output/Notations.out b/test-suite/output/Notations.out
index ada524f1..beba8df9 100644
--- a/test-suite/output/Notations.out
+++ b/test-suite/output/Notations.out
@@ -122,3 +122,8 @@ fun x : option Z => match x with
      : option Z -> Z
 s
      : s
+Identifier 'foo' now a keyword
+10
+     : nat
+fun _ : nat => 9
+     : nat -> nat
diff --git a/test-suite/output/Notations.v b/test-suite/output/Notations.v
index 4a2c411e..52f499ab 100644
--- a/test-suite/output/Notations.v
+++ b/test-suite/output/Notations.v
@@ -253,3 +253,12 @@ Check (fun x => match x with SOME3 x => x | NONE3 => 0 end).
 
 Notation s := Type.
 Check s.
+
+(* Test bug #2835: notations were not uniformly managed under prod and lambda *)
+
+Open Scope nat_scope.
+
+Notation "'foo' n" := (S n) (at level 50): nat_scope.
+
+Check (foo 9).
+Check (fun _ : nat => 9).
diff --git a/test-suite/output/ZSyntax.out b/test-suite/output/ZSyntax.out
index 1b7a2903..dc41b0aa 100644
--- a/test-suite/output/ZSyntax.out
+++ b/test-suite/output/ZSyntax.out
@@ -2,19 +2,19 @@
      : Z
 fun f : nat -> Z => (f 0%nat + 0)%Z
      : (nat -> Z) -> Z
-fun x : positive => Zpos x~0
+fun x : positive => Z.pos x~0
      : positive -> Z
-fun x : positive => (Zpos x + 1)%Z
+fun x : positive => (Z.pos x + 1)%Z
      : positive -> Z
-fun x : positive => Zpos x
+fun x : positive => Z.pos x
      : positive -> Z
-fun x : positive => Zneg x~0
+fun x : positive => Z.neg x~0
      : positive -> Z
-fun x : positive => (Zpos x~0 + 0)%Z
+fun x : positive => (Z.pos x~0 + 0)%Z
      : positive -> Z
-fun x : positive => (- Zpos x~0)%Z
+fun x : positive => (- Z.pos x~0)%Z
      : positive -> Z
-fun x : positive => (- Zpos x~0 + 0)%Z
+fun x : positive => (- Z.pos x~0 + 0)%Z
      : positive -> Z
 (Z.of_nat 0 + 1)%Z
      : Z
diff --git a/test-suite/success/Check.v b/test-suite/success/Check.v
index 47180ef6..21a9722d 100644
--- a/test-suite/success/Check.v
+++ b/test-suite/success/Check.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/Field.v b/test-suite/success/Field.v
index 0efd90a1..9301cd27 100644
--- a/test-suite/success/Field.v
+++ b/test-suite/success/Field.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/Funind.v b/test-suite/success/Funind.v
index b17adef6..ccce3bbe 100644
--- a/test-suite/success/Funind.v
+++ b/test-suite/success/Funind.v
@@ -9,7 +9,7 @@ Functional Scheme iszero_ind := Induction for iszero Sort Prop.
 
 Lemma toto : forall n : nat, n = 0 -> iszero n = true.
 intros x eg.
- functional induction iszero x; simpl in |- *.
+ functional induction iszero x; simpl.
 trivial.
 inversion eg.
 Qed.
@@ -212,19 +212,19 @@ Function plus_x_not_five'' (n m : nat) {struct n} : nat :=
 
 Lemma notplusfive'' : forall x y : nat, y = 5 -> plus_x_not_five'' x y = x.
 intros a b.
- functional induction plus_x_not_five'' a b; intros hyp; simpl in |- *; auto.
+ functional induction plus_x_not_five'' a b; intros hyp; simpl; auto.
 Qed.
 
 Lemma iseq_eq : forall n m : nat, n = m -> nat_equal_bool n m = true.
 intros n m.
- functional induction nat_equal_bool n m; simpl in |- *; intros hyp; auto.
+ functional induction nat_equal_bool n m; simpl; intros hyp; auto.
 rewrite <- hyp in y; simpl in y;tauto.
 inversion hyp.
 Qed.
 
 Lemma iseq_eq' : forall n m : nat, nat_equal_bool n m = true -> n = m.
 intros n m.
- functional induction nat_equal_bool n m; simpl in |- *; intros eg; auto.
+ functional induction nat_equal_bool n m; simpl; intros eg; auto.
 inversion eg.
 inversion eg.
 Qed.
@@ -245,7 +245,7 @@ Qed.
 
 Lemma inf_x_plusxy'' : forall x : nat, x <= x + 0.
 intros n.
-unfold plus in |- *.
+unfold plus.
  functional induction plus n 0; intros.
 auto with arith.
 apply le_n_S.
@@ -266,7 +266,7 @@ Function mod2 (n : nat) : nat :=
 
 Lemma princ_mod2 : forall n : nat, mod2 n <= n.
 intros n.
- functional induction mod2 n; simpl in |- *; auto with arith.
+ functional induction mod2 n; simpl; auto with arith.
 Qed.
 
 Function isfour (n : nat) : bool :=
@@ -284,7 +284,7 @@ Function isononeorfour (n : nat) : bool :=
 
 Lemma toto'' : forall n : nat, istrue (isfour n) -> istrue (isononeorfour n).
 intros n.
- functional induction isononeorfour n; intros istr; simpl in |- *;
+ functional induction isononeorfour n; intros istr; simpl;
  inversion istr.
 apply istrue0.
 destruct n. inversion istr.
@@ -367,7 +367,7 @@ Function ftest2 (n m : nat) {struct n} : nat :=
 
 Lemma test2' : forall n m : nat, ftest2 n m <= 2.
 intros n m.
- functional induction ftest2 n m; simpl in |- *; intros; auto.
+ functional induction ftest2 n m; simpl; intros; auto.
 Qed.
 
 Function ftest3 (n m : nat) {struct n} : nat :=
@@ -387,7 +387,7 @@ auto.
 intros.
 auto.
 intros.
-simpl in |- *.
+simpl.
 auto.
 Qed.
 
@@ -408,7 +408,7 @@ auto.
 intros.
 auto.
 intros.
-simpl in |- *.
+simpl.
 auto.
 Qed.
 
@@ -451,7 +451,7 @@ Qed.
 
 Lemma essai6 : forall n m : nat, ftest6 n m <= 2.
 intros n m.
- functional induction ftest6 n m; simpl in |- *; auto.
+ functional induction ftest6 n m; simpl; auto.
 Qed.
 
 (* Some tests with modules *)
diff --git a/test-suite/success/Hints.v b/test-suite/success/Hints.v
index 071fb957..cc8cec47 100644
--- a/test-suite/success/Hints.v
+++ b/test-suite/success/Hints.v
@@ -2,26 +2,26 @@
 (* Checks that qualified names are accepted *)
 
 (* New-style syntax *)
-Hint Resolve refl_equal: core arith.
-Hint Immediate trans_equal.
-Hint Unfold sym_equal: core.
+Hint Resolve eq_refl: core arith.
+Hint Immediate eq_trans.
+Hint Unfold eq_sym: core.
 Hint Constructors eq: foo bar.
-Hint Extern 3 (_ = _) => apply refl_equal: foo bar.
+Hint Extern 3 (_ = _) => apply eq_refl: foo bar.
 
 (* Old-style syntax *)
-Hint Resolve refl_equal sym_equal.
-Hint Resolve refl_equal sym_equal: foo.
-Hint Immediate refl_equal sym_equal.
-Hint Immediate refl_equal sym_equal: foo.
-Hint Unfold fst sym_equal.
-Hint Unfold fst sym_equal: foo.
+Hint Resolve eq_refl eq_sym.
+Hint Resolve eq_refl eq_sym: foo.
+Hint Immediate eq_refl eq_sym.
+Hint Immediate eq_refl eq_sym: foo.
+Hint Unfold fst eq_sym.
+Hint Unfold fst eq_sym: foo.
 
 (* Checks that local names are accepted *)
 Section A.
   Remark Refl : forall (A : Set) (x : A), x = x.
-  Proof. exact @refl_equal. Defined.
-  Definition Sym := sym_equal.
-  Let Trans := trans_equal.
+  Proof. exact @eq_refl. Defined.
+  Definition Sym := eq_sym.
+  Let Trans := eq_trans.
 
   Hint Resolve Refl: foo.
   Hint Resolve Sym: bar.
diff --git a/test-suite/success/LegacyField.v b/test-suite/success/LegacyField.v
index df4da431..d55ae384 100644
--- a/test-suite/success/LegacyField.v
+++ b/test-suite/success/LegacyField.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/MatchFail.v b/test-suite/success/MatchFail.v
index 660ca3cb..c2d87a44 100644
--- a/test-suite/success/MatchFail.v
+++ b/test-suite/success/MatchFail.v
@@ -12,13 +12,13 @@ Ltac compute_POS :=
       let v := constr:X1 in
       match constr:v with
       | 1%positive => fail 1
-      | _ =>  rewrite (BinInt.Zpos_xI v)
+      | _ =>  rewrite (BinInt.Pos2Z.inj_xI v)
       end
   |  |- context [(Zpos (xO ?X1))] =>
       let v := constr:X1 in
       match constr:v with
       | 1%positive => fail 1
-      | _ =>  rewrite (BinInt.Zpos_xO v)
+      | _ =>  rewrite (BinInt.Pos2Z.inj_xO v)
       end
   end.
 
diff --git a/test-suite/success/Mod_type.v b/test-suite/success/Mod_type.v
index b847833f..d5e1a38c 100644
--- a/test-suite/success/Mod_type.v
+++ b/test-suite/success/Mod_type.v
@@ -17,3 +17,15 @@ Module Bar : BAR.
   Module Foo := Fu.
 
 End Bar.
+
+(* Check bug #2809: correct printing of modules with notations *)
+
+Module C.
+  Inductive test : Type :=
+    | c1 : test
+    | c2 : nat -> test.
+
+  Notation "! x" := (c2 x) (at level 50).
+End C.
+
+Print C. (* Should print test_rect without failing *)
diff --git a/test-suite/success/Notations.v b/test-suite/success/Notations.v
index 89f11059..2371d32c 100644
--- a/test-suite/success/Notations.v
+++ b/test-suite/success/Notations.v
@@ -96,3 +96,8 @@ 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.
+
+(* Bug #2708: don't check for scope of variables used as binder *)
+
+Parameter traverse : (nat -> unit) -> (nat -> unit).
+Notation traverse_var f l := (traverse (fun l => f l) l).
diff --git a/test-suite/success/OmegaPre.v b/test-suite/success/OmegaPre.v
index f4996734..17531064 100644
--- a/test-suite/success/OmegaPre.v
+++ b/test-suite/success/OmegaPre.v
@@ -14,38 +14,38 @@ Open Scope Z_scope.
 
 (* zify_op *)
 
-Goal forall a:Z, Zmax a a = a.
+Goal forall a:Z, Z.max a a = a.
 intros.
 omega with *.
 Qed.
 
-Goal forall a b:Z, Zmax a b = Zmax b a.
+Goal forall a b:Z, Z.max a b = Z.max b a.
 intros.
 omega with *.
 Qed.
 
-Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c.
+Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c.
 intros.
 omega with *.
 Qed.
 
-Goal forall a b:Z, Zmax a b + Zmin a b = a + b.
+Goal forall a b:Z, Z.max a b + Z.min a b = a + b.
 intros.
 omega with *.
 Qed.
 
-Goal forall a:Z, (Zabs a)*(Zsgn a) = a.
+Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
 intros.
 zify.
 intuition; subst; omega. (* pure multiplication: omega alone can't do it *)
 Qed.
 
-Goal forall a:Z, Zabs a = a -> a >= 0.
+Goal forall a:Z, Z.abs a = a -> a >= 0.
 intros.
 omega with *.
 Qed.
 
-Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1.
+Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1.
 intros.
 omega with *.
 Qed.
@@ -119,7 +119,7 @@ Qed.
 
 (* mix of datatypes *)
 
-Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p.
+Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p.
 intros.
 omega with *.
 Qed.
diff --git a/test-suite/success/ProgramWf.v b/test-suite/success/ProgramWf.v
index 00a13aed..3b7f0d84 100644
--- a/test-suite/success/ProgramWf.v
+++ b/test-suite/success/ProgramWf.v
@@ -22,14 +22,14 @@ Program Fixpoint merge (n m : nat) {measure (n + m) (lt)} : nat :=
 Print merge.
 
 
-Print Zlt.
+Print Z.lt.
 Print Zwf.
 
-Open Local Scope Z_scope.
+Local Open Scope Z_scope.
 
 Program Fixpoint Zwfrec (n m : Z) {measure (n + m) (Zwf 0)} : Z :=
   match n ?= m with
-    | Lt => Zwfrec n (Zpred m)
+    | Lt => Zwfrec n (Z.pred m)
     | _ => 0
   end.
 
diff --git a/test-suite/success/ROmegaPre.v b/test-suite/success/ROmegaPre.v
index bd473fa6..fa659273 100644
--- a/test-suite/success/ROmegaPre.v
+++ b/test-suite/success/ROmegaPre.v
@@ -14,38 +14,38 @@ Open Scope Z_scope.
 
 (* zify_op *)
 
-Goal forall a:Z, Zmax a a = a.
+Goal forall a:Z, Z.max a a = a.
 intros.
 romega with *.
 Qed.
 
-Goal forall a b:Z, Zmax a b = Zmax b a.
+Goal forall a b:Z, Z.max a b = Z.max b a.
 intros.
 romega with *.
 Qed.
 
-Goal forall a b c:Z, Zmax a (Zmax b c) = Zmax (Zmax a b) c.
+Goal forall a b c:Z, Z.max a (Z.max b c) = Z.max (Z.max a b) c.
 intros.
 romega with *.
 Qed.
 
-Goal forall a b:Z, Zmax a b + Zmin a b = a + b.
+Goal forall a b:Z, Z.max a b + Z.min a b = a + b.
 intros.
 romega with *.
 Qed.
 
-Goal forall a:Z, (Zabs a)*(Zsgn a) = a.
+Goal forall a:Z, (Z.abs a)*(Z.sgn a) = a.
 intros.
 zify.
 intuition; subst; romega. (* pure multiplication: omega alone can't do it *)
 Qed.
 
-Goal forall a:Z, Zabs a = a -> a >= 0.
+Goal forall a:Z, Z.abs a = a -> a >= 0.
 intros.
 romega with *.
 Qed.
 
-Goal forall a:Z, Zsgn a = a -> a = 1 \/ a = 0 \/ a = -1.
+Goal forall a:Z, Z.sgn a = a -> a = 1 \/ a = 0 \/ a = -1.
 intros.
 romega with *.
 Qed.
@@ -119,7 +119,7 @@ Qed.
 
 (* mix of datatypes *)
 
-Goal forall p, Z_of_N (N_of_nat (nat_of_N (Npos p))) = Zpos p.
+Goal forall p, Z.of_N (N.of_nat (N.to_nat (Npos p))) = Zpos p.
 intros.
 romega with *.
 Qed.
diff --git a/test-suite/success/RecTutorial.v b/test-suite/success/RecTutorial.v
index 64048fe2..459645f6 100644
--- a/test-suite/success/RecTutorial.v
+++ b/test-suite/success/RecTutorial.v
@@ -378,18 +378,18 @@ Inductive itree : Set :=
 
 Definition isingle l := inode l (fun i => ileaf).
 
-Definition t1 := inode 0 (fun n => isingle (Z_of_nat (2*n))).
+Definition t1 := inode 0 (fun n => isingle (Z.of_nat (2*n))).
 
 Definition t2 := inode 0
                       (fun n : nat =>
-                               inode (Z_of_nat n)
-                                     (fun p => isingle (Z_of_nat (n*p)))).
+                               inode (Z.of_nat n)
+                                     (fun p => isingle (Z.of_nat (n*p)))).
 
 
 Inductive itree_le : itree-> itree -> Prop :=
   | le_leaf : forall t, itree_le  ileaf t
   | le_node  : forall l l' s s',
-                       Zle l l' ->
+                       Z.le l l' ->
                       (forall i, exists j:nat, itree_le (s i) (s' j)) ->
                       itree_le  (inode  l s) (inode  l' s').
 
@@ -424,7 +424,7 @@ Qed.
 Inductive itree_le' : itree-> itree -> Prop :=
   | le_leaf' : forall t, itree_le'  ileaf t
   | le_node' : forall l l' s s' g,
-                       Zle l l' ->
+                       Z.le l l' ->
                       (forall i, itree_le' (s i) (s' (g i))) ->
                        itree_le'  (inode  l s) (inode  l' s').
 
diff --git a/test-suite/success/Reg.v b/test-suite/success/Reg.v
index 89b3032c..c2d5cb2f 100644
--- a/test-suite/success/Reg.v
+++ b/test-suite/success/Reg.v
@@ -39,7 +39,7 @@ Lemma essai7 :
  derivable_pt (fun x : R => (cos (/ sqrt x) * Rsqr (sin x + 1))%R) 1.
 reg.
 apply Rlt_0_1.
-red in |- *; intro;  rewrite sqrt_1 in H; assert (H0 := R1_neq_R0); elim H0;
+red; intro;  rewrite sqrt_1 in H; assert (H0 := R1_neq_R0); elim H0;
  assumption.
 Qed.
 
@@ -127,7 +127,7 @@ Lemma essai23 :
    (fun x : R => (sin (sqrt (x - 1)) + exp (Rsqr (sqrt x + 3)))%R) 1.
 reg.
 left; apply Rlt_0_1.
-right; unfold Rminus in |- *;  rewrite Rplus_opp_r; reflexivity.
+right; unfold Rminus;  rewrite Rplus_opp_r; reflexivity.
 Qed.
 
 Lemma essai24 :
@@ -135,8 +135,8 @@ Lemma essai24 :
 reg.
  replace (x * x + 2 * x + 2)%R with (Rsqr (x + 1) + 1)%R.
 apply Rplus_le_lt_0_compat; [ apply Rle_0_sqr | apply Rlt_0_1 ].
-unfold Rsqr in |- *;  ring.
-red in |- *; intro; cut (0 < x * x + 1)%R.
+unfold Rsqr;  ring.
+red; intro; cut (0 < x * x + 1)%R.
 intro;  rewrite H in H0; elim (Rlt_irrefl _ H0).
 apply Rplus_le_lt_0_compat;
  [  replace (x * x)%R with (Rsqr x); [ apply Rle_0_sqr | reflexivity ]
diff --git a/test-suite/success/Scopes.v b/test-suite/success/Scopes.v
index 55d8343e..a79d28fa 100644
--- a/test-suite/success/Scopes.v
+++ b/test-suite/success/Scopes.v
@@ -3,6 +3,6 @@
 Require Import ZArith.
 
 Module A.
-Definition opp := Zopp.
+Definition opp := Z.opp.
 End A.
 Check (A.opp 3).
diff --git a/test-suite/success/Tauto.v b/test-suite/success/Tauto.v
index c4e67677..73ef3720 100644
--- a/test-suite/success/Tauto.v
+++ b/test-suite/success/Tauto.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/TestRefine.v b/test-suite/success/TestRefine.v
index 705bdc45..e9d6a969 100644
--- a/test-suite/success/TestRefine.v
+++ b/test-suite/success/TestRefine.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/Try.v b/test-suite/success/Try.v
index b356f277..361c787e 100644
--- a/test-suite/success/Try.v
+++ b/test-suite/success/Try.v
@@ -2,7 +2,7 @@
    non-existent names in Unfold [cf bug #263] *)
 
 Lemma lem1 : True.
-try unfold i_dont_exist in |- *.
+try unfold i_dont_exist.
 trivial.
 Qed.
 
diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v
index d3c76101..0d8bf556 100644
--- a/test-suite/success/apply.v
+++ b/test-suite/success/apply.v
@@ -8,8 +8,8 @@ Qed.
 
 Require Import ZArith.
 Goal (forall x y z, ~ z <= 0 -> x * z < y * z -> x <= y)%Z.
-intros; apply Znot_le_gt, Zgt_lt in H.
-apply Zmult_lt_reg_r, Zlt_le_weak in H0; auto.
+intros; apply Znot_le_gt, Z.gt_lt in H.
+apply Zmult_lt_reg_r, Z.lt_le_incl in H0; auto.
 Qed.
 
 (* Test application under tuples *)
@@ -266,7 +266,7 @@ Qed.
   (* This works because unfold calls clos_norm_flags which calls nf_evar *)
 
 Lemma eapply_evar_unfold : let x:=O in O=x -> 0=O.
-intros x H; eapply trans_equal;
+intros x H; eapply eq_trans;
 [apply H | unfold x;match goal with |- ?x = ?x => reflexivity end].
 Qed.
 
diff --git a/test-suite/success/change.v b/test-suite/success/change.v
index c65cf303..7bed7ecb 100644
--- a/test-suite/success/change.v
+++ b/test-suite/success/change.v
@@ -14,7 +14,7 @@ Abort.
 (* Check the combination of at, with and in (see bug #2146) *)
 
 Goal 3=3 -> 3=3. intro H.
-change 3 at 2 with (1+2) in |- *.
+change 3 at 2 with (1+2).
 change 3 at 2 with (1+2) in H |-.
 change 3 with (1+2) in H at 1 |- * at 1.
 (* Now check that there are no more 3's *)
@@ -25,10 +25,10 @@ Qed.
 change 3 at 1 with (1+2) at 3.
 change 3 at 1 with (1+2) in *.
 change 3 at 1 with (1+2) in H at 2 |-.
-change 3 at 1 with (1+2) in |- * at 3.
+change 3 at 1 with (1+2) at 3.
 change 3 at 1 with (1+2) in H |- *.
 change 3 at 1 with (1+2) in H, H|-.
-change 3 in |- * at 1.
+change 3 at 1.
  *)
 
 (* Test that pretyping checks allowed elimination sorts *)
diff --git a/test-suite/success/decl_mode.v b/test-suite/success/decl_mode.v
index bc1757fd..52575eca 100644
--- a/test-suite/success/decl_mode.v
+++ b/test-suite/success/decl_mode.v
@@ -138,7 +138,7 @@ Coercion IZR: Z >->R.*)
 Open Scope R_scope.
 
 Lemma square_abs_square:
-  forall p,(INR (Zabs_nat p) * INR (Zabs_nat p)) = (IZR p * IZR p).
+  forall p,(INR (Z.abs_nat p) * INR (Z.abs_nat p)) = (IZR p * IZR p).
 proof.
   assume p:Z.
   per cases on p.
@@ -147,7 +147,7 @@ proof.
     suppose it is (Zpos z).
       thus thesis.
     suppose it is (Zneg z).
-      have ((INR (Zabs_nat (Zneg z)) * INR (Zabs_nat (Zneg z))) =
+      have ((INR (Z.abs_nat (Zneg z)) * INR (Z.abs_nat (Zneg z))) =
       (IZR (Zpos z) * IZR (Zpos z))).
            ~= ((- IZR (Zpos z)) * (- IZR (Zpos z))).
       thus ~= (IZR (Zneg z) * IZR (Zneg z)).
@@ -165,15 +165,15 @@ proof.
   have H_in_R:(INR q<>0:>R) by H.
   have triv:((IZR p/INR q* INR q) =IZR p :>R) by * using field.
   have sqrt2:((sqrt (INR 2%nat) * sqrt (INR 2%nat))= INR 2%nat:>R) by sqrt_def.
-  have (INR (Zabs_nat p * Zabs_nat p)
-     = (INR (Zabs_nat p) * INR (Zabs_nat p)))
+  have (INR (Z.abs_nat p * Z.abs_nat p)
+     = (INR (Z.abs_nat p) * INR (Z.abs_nat p)))
     by mult_INR.
     ~=  (IZR p* IZR p) by square_abs_square.
     ~=  ((IZR p/INR q*INR q)*(IZR p/INR q*INR q)) by triv. (* we have to factor because field is too weak *)
     ~=  ((IZR p/INR q)*(IZR p/INR q)*(INR q*INR q)) using ring.
     ~=  (sqrt (INR 2%nat) * sqrt (INR 2%nat)*(INR q*INR q)) by H0.
     ~= (INR (2%nat * (q*q)))  by sqrt2,mult_INR.
-  then  (Zabs_nat p * Zabs_nat p = 2* (q * q))%nat.
+  then  (Z.abs_nat p * Z.abs_nat p = 2* (q * q))%nat.
     ~= ((q*q)+(q*q))%nat.
     ~= (Div2.double (q*q)).
   then (q=0%nat) by main_theorem.
diff --git a/test-suite/success/dependentind.v b/test-suite/success/dependentind.v
index 79d12a06..12ddbda8 100644
--- a/test-suite/success/dependentind.v
+++ b/test-suite/success/dependentind.v
@@ -68,7 +68,7 @@ where " Γ ⊢ τ " := (term Γ τ) : type_scope.
 
 Hint Constructors term : lambda.
 
-Open Local Scope context_scope.
+Local Open Scope context_scope.
 
 Ltac eqns := subst ; reverse ; simplify_dep_elim ; simplify_IH_hyps.
 
diff --git a/test-suite/success/eauto.v b/test-suite/success/eauto.v
index a94d8b1d..49bf8b15 100644
--- a/test-suite/success/eauto.v
+++ b/test-suite/success/eauto.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v
index 8c00583e..df73383a 100644
--- a/test-suite/success/eqdecide.v
+++ b/test-suite/success/eqdecide.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/extraction.v b/test-suite/success/extraction.v
index 3f8a3bc4..acd1da66 100644
--- a/test-suite/success/extraction.v
+++ b/test-suite/success/extraction.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/fix.v b/test-suite/success/fix.v
index b25b502c..8623f718 100644
--- a/test-suite/success/fix.v
+++ b/test-suite/success/fix.v
@@ -9,16 +9,16 @@ Inductive rBoolOp : Set :=
   | rAnd : rBoolOp
   | rEq : rBoolOp.
 
-Definition rlt (a b : rNat) : Prop := Pcompare a b Eq = Lt.
+Definition rlt (a b : rNat) : Prop := Pos.compare_cont a b Eq = Lt.
 
 Definition rltDec : forall m n : rNat, {rlt m n} + {rlt n m \/ m = n}.
 intros n m; generalize (nat_of_P_lt_Lt_compare_morphism n m);
  generalize (nat_of_P_gt_Gt_compare_morphism n m);
- generalize (Pcompare_Eq_eq n m); case (Pcompare n m Eq).
+ generalize (Pcompare_Eq_eq n m); case (Pos.compare_cont n m Eq).
 intros H' H'0 H'1; right; right; auto.
-intros H' H'0 H'1; left; unfold rlt in |- *.
+intros H' H'0 H'1; left; unfold rlt.
 apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
-intros H' H'0 H'1; right; left; unfold rlt in |- *.
+intros H' H'0 H'1; right; left; unfold rlt.
 apply nat_of_P_lt_Lt_compare_complement_morphism; auto.
 apply H'0; auto.
 Defined.
diff --git a/test-suite/success/inds_type_sec.v b/test-suite/success/inds_type_sec.v
index 234c4223..9316ac03 100644
--- a/test-suite/success/inds_type_sec.v
+++ b/test-suite/success/inds_type_sec.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/induct.v b/test-suite/success/induct.v
index b24ed2f1..cc8e8dd8 100644
--- a/test-suite/success/induct.v
+++ b/test-suite/success/induct.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v
index 7387add6..c2eb8bd7 100644
--- a/test-suite/success/ltac.v
+++ b/test-suite/success/ltac.v
@@ -2,7 +2,7 @@
 
 (* Submitted by Pierre Crégut *)
 (* Checks substitution of x *)
-Ltac f x := unfold x in |- *; idtac.
+Ltac f x := unfold x; idtac.
 
 Lemma lem1 : 0 + 0 = 0.
 f plus.
@@ -86,7 +86,7 @@ assert t.
 exact H.
 intro H1.
 apply H.
-symmetry  in |- *.
+symmetry .
 assumption.
 Qed.
 
@@ -105,7 +105,7 @@ sym'.
 exact H.
 intro H1.
 apply H.
-symmetry  in |- *.
+symmetry .
 assumption.
 Qed.
 
@@ -193,7 +193,7 @@ Abort.
 (* Used to fail in V8.1 *)
 
 Tactic Notation "test" constr(t) integer(n) :=
-   set (k := t) in |- * at n.
+   set (k := t) at n.
 
 Goal forall x : nat, x = 1 -> x + x + x = 3.
 intros x H.
diff --git a/test-suite/success/mutual_ind.v b/test-suite/success/mutual_ind.v
index fcadd150..5fe760bf 100644
--- a/test-suite/success/mutual_ind.v
+++ b/test-suite/success/mutual_ind.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/proof_using.v b/test-suite/success/proof_using.v
index 93a9ef11..bf302df4 100644
--- a/test-suite/success/proof_using.v
+++ b/test-suite/success/proof_using.v
@@ -51,11 +51,17 @@ Proof using v1 v2.
 admit.
 Qed.
 
+Lemma deep2 : v1 = v2.
+Proof using v1 v2.
+Admitted.
+
 End S2.
 
 Check (deep 3 : v1 = 3).
+Check (deep2 3 : v1 = 3).
 
 End S1.
 
 Check (deep 3 4 : 3 = 4).
+Check (deep2 3 4 : 3 = 4).
 
diff --git a/test-suite/success/remember.v b/test-suite/success/remember.v
index 3241e133..5f8ed03d 100644
--- a/test-suite/success/remember.v
+++ b/test-suite/success/remember.v
@@ -4,5 +4,5 @@ Lemma A : forall (P: forall X, X -> Prop), P nat 0 -> P nat 0.
 intros.
 Fail remember nat as X.
 Fail remember nat as X in H. (* This line used to succeed in 8.3 *)
-Fail remember nat as X in |- *.
+Fail remember nat as X.
 Abort.
diff --git a/test-suite/success/searchabout.v b/test-suite/success/searchabout.v
index d9ade314..9edfd825 100644
--- a/test-suite/success/searchabout.v
+++ b/test-suite/success/searchabout.v
@@ -55,6 +55,6 @@ SearchAbout [-"*"%nat "+"%nat] outside Logic.
 
 Require Import ZArith.
 
-SearchAbout Zmult Zplus "distr".
+SearchAbout Z.mul Z.add "distr".
 SearchAbout "+"%Z "*"%Z "distr" -positive -Prop.
 SearchAbout (?x * _ + ?x * _)%Z outside OmegaLemmas.
diff --git a/test-suite/success/setoid_test.v b/test-suite/success/setoid_test.v
index 19693d70..653b5bf9 100644
--- a/test-suite/success/setoid_test.v
+++ b/test-suite/success/setoid_test.v
@@ -18,10 +18,10 @@ Definition same (s t : set) : Prop := forall a : A, In a s <-> In a t.
 
 Lemma setoid_set : Setoid_Theory set same.
 
-unfold same in |- *; split ; red.
-red in |- *; auto.
+unfold same; split ; red.
+red; auto.
 
-red in |- *.
+red.
 intros.
 elim (H a); auto.
 
@@ -33,19 +33,19 @@ Qed.
 Add Setoid set same setoid_set as setsetoid.
 
 Add Morphism In : In_ext.
-unfold same in |- *; intros a s t H; elim (H a); auto.
+unfold same; intros a s t H; elim (H a); auto.
 Qed.
 
 Lemma add_aux :
  forall s t : set,
  same s t -> forall a b : A, In a (Add b s) -> In a (Add b t).
-unfold same in |- *; simple induction 2; intros.
+unfold same; simple induction 2; intros.
 rewrite H1.
-simpl in |- *; left; reflexivity.
+simpl; left; reflexivity.
 
 elim (H a).
 intros.
-simpl in |- *; right.
+simpl; right.
 apply (H2 H1).
 Qed.
 
@@ -74,15 +74,15 @@ setoid_replace (remove a (Add a Empty)) with Empty.
 
 auto.
 
-unfold same in |- *.
+unfold same.
 split.
-simpl in |- *.
+simpl.
 case (eq_dec a a).
 intros e ff; elim ff.
 
 intros; absurd (a = a); trivial.
 
-simpl in |- *.
+simpl.
 intro H; elim H.
 Qed.
 
diff --git a/test-suite/success/specialize.v b/test-suite/success/specialize.v
index 57837321..c5f032be 100644
--- a/test-suite/success/specialize.v
+++ b/test-suite/success/specialize.v
@@ -5,20 +5,20 @@ intros.
 (* "compatibility" mode: specializing a global name
    means a kind of generalize *)
 
-specialize trans_equal. intros _.
-specialize trans_equal with (1:=H)(2:=H0). intros _.
-specialize trans_equal with (x:=a)(y:=b)(z:=c). intros _.
-specialize trans_equal with (1:=H)(z:=c). intros _.
-specialize trans_equal with nat a b c. intros _.
-specialize (@trans_equal nat). intros _.
-specialize (@trans_equal _ a b c). intros _.
-specialize (trans_equal (x:=a)). intros _.
-specialize (trans_equal (x:=a)(y:=b)). intros _.
-specialize (trans_equal H H0). intros _.
-specialize (trans_equal H0 (z:=b)). intros _.
+specialize eq_trans. intros _.
+specialize eq_trans with (1:=H)(2:=H0). intros _.
+specialize eq_trans with (x:=a)(y:=b)(z:=c). intros _.
+specialize eq_trans with (1:=H)(z:=c). intros _.
+specialize eq_trans with nat a b c. intros _.
+specialize (@eq_trans nat). intros _.
+specialize (@eq_trans _ a b c). intros _.
+specialize (eq_trans (x:=a)). intros _.
+specialize (eq_trans (x:=a)(y:=b)). intros _.
+specialize (eq_trans H H0). intros _.
+specialize (eq_trans H0 (z:=b)). intros _.
 
 (* local "in place" specialization *)
-assert (Eq:=trans_equal).
+assert (Eq:=eq_trans).
 
 specialize Eq.
 specialize Eq with (1:=H)(2:=H0). Undo.
@@ -38,10 +38,10 @@ specialize (Eq _ _ _ b H0). Undo.
     presque ok... *)
 
 (* 2) echoue moins lorsque zero premise de mangé *)
-specialize trans_equal with (1:=Eq).  (* mal typé !! *)
+specialize eq_trans with (1:=Eq).  (* mal typé !! *)
 
 (* 3) *)
-specialize trans_equal with _ a b c. intros _.
+specialize eq_trans with _ a b c. intros _.
 (* Anomaly: Evar ?88 was not declared. Please report. *)
 *)
 
diff --git a/test-suite/success/unfold.v b/test-suite/success/unfold.v
index 5649e2f7..62ecb1aa 100644
--- a/test-suite/success/unfold.v
+++ b/test-suite/success/unfold.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
diff --git a/test-suite/success/unicode_utf8.v b/test-suite/success/unicode_utf8.v
index 8b7764e5..42e32ccc 100644
--- a/test-suite/success/unicode_utf8.v
+++ b/test-suite/success/unicode_utf8.v
@@ -75,7 +75,7 @@ Notation "x ≤ y" := (x<=y) (at level 70, no associativity).
 
 Require Import ZArith.
 Open Scope Z_scope.
-Locate "≤". (* still le, not Zle *)
+Locate "≤". (* still le, not Z.le *)
 Notation "x ≤ y" := (x<=y) (at level 70, no associativity).
 Locate "≤".
 Close Scope Z_scope.
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v
index 469cbeb7..e00701fb 100644
--- a/test-suite/success/univers.v
+++ b/test-suite/success/univers.v
@@ -16,7 +16,7 @@ auto.
 Qed.
 
 Lemma lem3 : forall P : Prop, P.
-intro P; pattern P in |- *.
+intro P; pattern P.
 apply lem2.
 Abort.
 
@@ -34,7 +34,7 @@ Require Import Relations.
 
 Theorem dep_eq_trans : forall X : Type, transitive X (dep_eq X).
 Proof.
-  unfold transitive in |- *.
+  unfold transitive.
   intros X f g h H1 H2.
   inversion H1.
 Abort.
diff --git a/test-suite/typeclasses/NewSetoid.v b/test-suite/typeclasses/NewSetoid.v
index 3fdcce6f..63f5d985 100644
--- a/test-suite/typeclasses/NewSetoid.v
+++ b/test-suite/typeclasses/NewSetoid.v
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)