Imported Upstream version 8.6

109 files changed, 1239 insertions, 580 deletions

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index f998e861..58d3a2b3 100644
--- a/theories/Arith/Between.v
+++ b/theories/Arith/Between.v
@@ -20,20 +20,20 @@ Section Between.
     | bet_emp : between k k
     | bet_S : forall l, between k l -> P l -> between k (S l).
 
-  Hint Constructors between: arith v62.
+  Hint Constructors between: arith.
 
   Lemma bet_eq : forall k l, l = k -> between k l.
   Proof.
     induction 1; auto with arith.
   Qed.
 
-  Hint Resolve bet_eq: arith v62.
+  Hint Resolve bet_eq: arith.
 
   Lemma between_le : forall k l, between k l -> k <= l.
   Proof.
     induction 1; auto with arith.
   Qed.
-  Hint Immediate between_le: arith v62.
+  Hint Immediate between_le: arith.
 
   Lemma between_Sk_l : forall k l, between k l -> S k <= l -> between (S k) l.
   Proof.
@@ -41,7 +41,7 @@ Section Between.
     intros; absurd (S k <= k); auto with arith.
     destruct H; auto with arith.
   Qed.
-  Hint Resolve between_Sk_l: arith v62.
+  Hint Resolve between_Sk_l: arith.
 
   Lemma between_restr :
     forall k l (m:nat), k <= l -> l <= m -> between k m -> between l m.
@@ -53,7 +53,7 @@ Section Between.
     | exists_S : forall l, exists_between k l -> exists_between k (S l)
     | exists_le : forall l, k <= l -> Q l -> exists_between k (S l).
 
-  Hint Constructors exists_between: arith v62.
+  Hint Constructors exists_between: arith.
 
   Lemma exists_le_S : forall k l, exists_between k l -> S k <= l.
   Proof.
@@ -62,13 +62,13 @@ Section Between.
 
   Lemma exists_lt : forall k l, exists_between k l -> k < l.
   Proof exists_le_S.
-  Hint Immediate exists_le_S exists_lt: arith v62.
+  Hint Immediate exists_le_S exists_lt: arith.
 
   Lemma exists_S_le : forall k l, exists_between k (S l) -> k <= l.
   Proof.
     intros; apply le_S_n; auto with arith.
   Qed.
-  Hint Immediate exists_S_le: arith v62.
+  Hint Immediate exists_S_le: arith.
 
   Definition in_int p q r := p <= r /\ r < q.
 
@@ -76,7 +76,7 @@ Section Between.
   Proof.
     red; auto with arith.
   Qed.
-  Hint Resolve in_int_intro: arith v62.
+  Hint Resolve in_int_intro: arith.
 
   Lemma in_int_lt : forall p q r, in_int p q r -> p < q.
   Proof.
@@ -95,13 +95,13 @@ Section Between.
   Proof.
     induction 1; auto with arith.
   Qed.
-  Hint Resolve in_int_S: arith v62.
+  Hint Resolve in_int_S: arith.
 
   Lemma in_int_Sp_q : forall p q r, in_int (S p) q r -> in_int p q r.
   Proof.
     induction 1; auto with arith.
   Qed.
-  Hint Immediate in_int_Sp_q: arith v62.
+  Hint Immediate in_int_Sp_q: arith.
 
   Lemma between_in_int :
     forall k l, between k l -> forall r, in_int k l r -> P r.
@@ -183,5 +183,5 @@ Section Between.
 End Between.
 
 Hint Resolve nth_O bet_S bet_emp bet_eq between_Sk_l exists_S exists_le
-  in_int_S in_int_intro: arith v62.
-Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith v62.
+  in_int_S in_int_intro: arith.
+Hint Immediate in_int_Sp_q exists_le_S exists_S_le: arith.
diff --git a/theories/Arith/EqNat.v b/theories/Arith/EqNat.v
index 206fc0ab..f998c19f 100644
--- a/theories/Arith/EqNat.v
+++ b/theories/Arith/EqNat.v
@@ -25,7 +25,7 @@ Theorem eq_nat_refl n : eq_nat n n.
 Proof.
   induction n; simpl; auto.
 Qed.
-Hint Resolve eq_nat_refl: arith v62.
+Hint Resolve eq_nat_refl: arith.
 
 (** [eq] restricted to [nat] and [eq_nat] are equivalent *)
 
@@ -46,7 +46,7 @@ Proof.
  apply eq_nat_is_eq.
 Qed.
 
-Hint Immediate eq_eq_nat eq_nat_eq: arith v62.
+Hint Immediate eq_eq_nat eq_nat_eq: arith.
 
 Theorem eq_nat_elim :
   forall n (P:nat -> Prop), P n -> forall m, eq_nat n m -> P m.
diff --git a/theories/Arith/Gt.v b/theories/Arith/Gt.v
index dfd57694..67c94fdf 100644
--- a/theories/Arith/Gt.v
+++ b/theories/Arith/Gt.v
@@ -133,14 +133,14 @@ Qed.
 
 (** * Hints *)
 
-Hint Resolve gt_Sn_O gt_Sn_n gt_n_S : arith v62.
-Hint Immediate gt_S_n gt_pred : arith v62.
-Hint Resolve gt_irrefl gt_asym : arith v62.
-Hint Resolve le_not_gt gt_not_le : arith v62.
-Hint Immediate le_S_gt gt_S_le : arith v62.
-Hint Resolve gt_le_S le_gt_S : arith v62.
-Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith v62.
-Hint Resolve plus_gt_compat_l: arith v62.
+Hint Resolve gt_Sn_O gt_Sn_n gt_n_S : arith.
+Hint Immediate gt_S_n gt_pred : arith.
+Hint Resolve gt_irrefl gt_asym : arith.
+Hint Resolve le_not_gt gt_not_le : arith.
+Hint Immediate le_S_gt gt_S_le : arith.
+Hint Resolve gt_le_S le_gt_S : arith.
+Hint Resolve gt_trans_S le_gt_trans gt_le_trans: arith.
+Hint Resolve plus_gt_compat_l: arith.
 
 (* begin hide *)
 Notation gt_O_eq := gt_0_eq (only parsing).
diff --git a/theories/Arith/Le.v b/theories/Arith/Le.v
index ceb91187..0fbcec57 100644
--- a/theories/Arith/Le.v
+++ b/theories/Arith/Le.v
@@ -30,8 +30,8 @@ Notation le_refl := Nat.le_refl (compat "8.4").
 Notation le_trans := Nat.le_trans (compat "8.4").
 Notation le_antisym := Nat.le_antisymm (compat "8.4").
 
-Hint Resolve le_trans: arith v62.
-Hint Immediate le_antisym: arith v62.
+Hint Resolve le_trans: arith.
+Hint Immediate le_antisym: arith.
 
 (** * Properties of [le] w.r.t 0 *)
 
@@ -59,16 +59,16 @@ Notation le_Sn_n := Nat.nle_succ_diag_l (compat "8.4"). (* ~ S n <= n *)
 Theorem le_Sn_le : forall n m, S n <= m -> n <= m.
 Proof Nat.lt_le_incl.
 
-Hint Resolve le_0_n le_Sn_0: arith v62.
-Hint Resolve le_n_S le_n_Sn le_Sn_n : arith v62.
-Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith v62.
+Hint Resolve le_0_n le_Sn_0: arith.
+Hint Resolve le_n_S le_n_Sn le_Sn_n : arith.
+Hint Immediate le_n_0_eq le_Sn_le le_S_n : arith.
 
 (** * Properties of [le] w.r.t predecessor *)
 
 Notation le_pred_n := Nat.le_pred_l (compat "8.4"). (* pred n <= n *)
 Notation le_pred := Nat.pred_le_mono (compat "8.4"). (* n<=m -> pred n <= pred m *)
 
-Hint Resolve le_pred_n: arith v62.
+Hint Resolve le_pred_n: arith.
 
 (** * A different elimination principle for the order on natural numbers *)
 
diff --git a/theories/Arith/Lt.v b/theories/Arith/Lt.v
index f824ee6f..bfc2b91a 100644
--- a/theories/Arith/Lt.v
+++ b/theories/Arith/Lt.v
@@ -25,7 +25,7 @@ Local Open Scope nat_scope.
 
 Notation lt_irrefl := Nat.lt_irrefl (compat "8.4"). (* ~ x < x *)
 
-Hint Resolve lt_irrefl: arith v62.
+Hint Resolve lt_irrefl: arith.
 
 (** * Relationship between [le] and [lt] *)
 
@@ -44,9 +44,9 @@ Proof.
  apply Nat.lt_succ_r.
 Qed.
 
-Hint Immediate lt_le_S: arith v62.
-Hint Immediate lt_n_Sm_le: arith v62.
-Hint Immediate le_lt_n_Sm: arith v62.
+Hint Immediate lt_le_S: arith.
+Hint Immediate lt_n_Sm_le: arith.
+Hint Immediate le_lt_n_Sm: arith.
 
 Theorem le_not_lt n m : n <= m -> ~ m < n.
 Proof.
@@ -58,7 +58,7 @@ Proof.
  apply Nat.lt_nge.
 Qed.
 
-Hint Immediate le_not_lt lt_not_le: arith v62.
+Hint Immediate le_not_lt lt_not_le: arith.
 
 (** * Asymmetry *)
 
@@ -79,8 +79,8 @@ Proof.
  intros. now apply Nat.neq_sym, Nat.neq_0_lt_0.
 Qed.
 
-Hint Resolve lt_0_Sn lt_n_0 : arith v62.
-Hint Immediate neq_0_lt lt_0_neq: arith v62.
+Hint Resolve lt_0_Sn lt_n_0 : arith.
+Hint Immediate neq_0_lt lt_0_neq: arith.
 
 (** * Order and successor *)
 
@@ -97,8 +97,8 @@ Proof.
  apply Nat.succ_lt_mono.
 Qed.
 
-Hint Resolve lt_n_Sn lt_S lt_n_S : arith v62.
-Hint Immediate lt_S_n : arith v62.
+Hint Resolve lt_n_Sn lt_S lt_n_S : arith.
+Hint Immediate lt_S_n : arith.
 
 (** * Predecessor *)
 
@@ -117,8 +117,8 @@ Proof.
  intros. now apply Nat.lt_pred_l, Nat.neq_0_lt_0.
 Qed.
 
-Hint Immediate lt_pred: arith v62.
-Hint Resolve lt_pred_n_n: arith v62.
+Hint Immediate lt_pred: arith.
+Hint Resolve lt_pred_n_n: arith.
 
 (** * Transitivity properties *)
 
@@ -126,7 +126,7 @@ Notation lt_trans := Nat.lt_trans (compat "8.4").
 Notation lt_le_trans := Nat.lt_le_trans (compat "8.4").
 Notation le_lt_trans := Nat.le_lt_trans (compat "8.4").
 
-Hint Resolve lt_trans lt_le_trans le_lt_trans: arith v62.
+Hint Resolve lt_trans lt_le_trans le_lt_trans: arith.
 
 (** * Large = strict or equal *)
 
@@ -139,7 +139,7 @@ Qed.
 
 Notation lt_le_weak := Nat.lt_le_incl (compat "8.4").
 
-Hint Immediate lt_le_weak: arith v62.
+Hint Immediate lt_le_weak: arith.
 
 (** * Dichotomy *)
 
diff --git a/theories/Arith/Max.v b/theories/Arith/Max.v
index 65534b2e..49152549 100644
--- a/theories/Arith/Max.v
+++ b/theories/Arith/Max.v
@@ -42,7 +42,7 @@ Notation max_SS := Nat.succ_max_distr (only parsing).
 (* end hide *)
 
 Hint Resolve
- Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r : arith v62.
+ Nat.max_l Nat.max_r Nat.le_max_l Nat.le_max_r : arith.
 
 Hint Resolve
- Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r : arith v62.
+ Nat.min_l Nat.min_r Nat.le_min_l Nat.le_min_r : arith.
diff --git a/theories/Arith/Minus.v b/theories/Arith/Minus.v
index bc3a318c..1fc8f790 100644
--- a/theories/Arith/Minus.v
+++ b/theories/Arith/Minus.v
@@ -107,13 +107,13 @@ Qed.
 
 (** * Hints *)
 
-Hint Resolve minus_n_O: arith v62.
-Hint Resolve minus_Sn_m: arith v62.
-Hint Resolve minus_diag_reverse: arith v62.
-Hint Resolve minus_plus_simpl_l_reverse: arith v62.
-Hint Immediate plus_minus: arith v62.
-Hint Resolve minus_plus: arith v62.
-Hint Resolve le_plus_minus: arith v62.
-Hint Resolve le_plus_minus_r: arith v62.
-Hint Resolve lt_minus: arith v62.
-Hint Immediate lt_O_minus_lt: arith v62.
+Hint Resolve minus_n_O: arith.
+Hint Resolve minus_Sn_m: arith.
+Hint Resolve minus_diag_reverse: arith.
+Hint Resolve minus_plus_simpl_l_reverse: arith.
+Hint Immediate plus_minus: arith.
+Hint Resolve minus_plus: arith.
+Hint Resolve le_plus_minus: arith.
+Hint Resolve le_plus_minus_r: arith.
+Hint Resolve lt_minus: arith.
+Hint Immediate lt_O_minus_lt: arith.
diff --git a/theories/Arith/Mult.v b/theories/Arith/Mult.v
index 96581243..a173efc1 100644
--- a/theories/Arith/Mult.v
+++ b/theories/Arith/Mult.v
@@ -31,13 +31,13 @@ Notation mult_0_r := Nat.mul_0_r (compat "8.4"). (* n * 0 = 0 *)
 Notation mult_1_l := Nat.mul_1_l (compat "8.4"). (* 1 * n = n *)
 Notation mult_1_r := Nat.mul_1_r (compat "8.4"). (* n * 1 = n *)
 
-Hint Resolve mult_1_l mult_1_r: arith v62.
+Hint Resolve mult_1_l mult_1_r: arith.
 
 (** ** Commutativity *)
 
 Notation mult_comm := Nat.mul_comm (compat "8.4"). (* n * m = m * n *)
 
-Hint Resolve mult_comm: arith v62.
+Hint Resolve mult_comm: arith.
 
 (** ** Distributivity *)
 
@@ -53,9 +53,9 @@ Notation mult_minus_distr_r :=
 Notation mult_minus_distr_l :=
   Nat.mul_sub_distr_l (compat "8.4"). (* n*(m-p) = n*m - n*p *)
 
-Hint Resolve mult_plus_distr_r: arith v62.
-Hint Resolve mult_minus_distr_r: arith v62.
-Hint Resolve mult_minus_distr_l: arith v62.
+Hint Resolve mult_plus_distr_r: arith.
+Hint Resolve mult_minus_distr_r: arith.
+Hint Resolve mult_minus_distr_l: arith.
 
 (** ** Associativity *)
 
@@ -66,8 +66,8 @@ Proof.
  symmetry. apply Nat.mul_assoc.
 Qed.
 
-Hint Resolve mult_assoc_reverse: arith v62.
-Hint Resolve mult_assoc: arith v62.
+Hint Resolve mult_assoc_reverse: arith.
+Hint Resolve mult_assoc: arith.
 
 (** ** Inversion lemmas *)
 
@@ -92,7 +92,7 @@ Lemma mult_O_le n m : m = 0 \/ n <= m * n.
 Proof.
  destruct m; [left|right]; simpl; trivial using Nat.le_add_r.
 Qed.
-Hint Resolve mult_O_le: arith v62.
+Hint Resolve mult_O_le: arith.
 
 Lemma mult_le_compat_l n m p : n <= m -> p * n <= p * m.
 Proof.
diff --git a/theories/Arith/Peano_dec.v b/theories/Arith/Peano_dec.v
index 340a7968..f8020a50 100644
--- a/theories/Arith/Peano_dec.v
+++ b/theories/Arith/Peano_dec.v
@@ -38,8 +38,7 @@ intros m n.
 generalize (eq_refl (S n)).
 generalize n at -1.
 induction (S n) as [|n0 IHn0]; try discriminate.
-clear n; intros n H; injection H; clear H; intro H.
-rewrite <- H; intros le_mn1 le_mn2; clear n H.
+clear n; intros n [= <-] le_mn1 le_mn2.
 pose (def_n2 := eq_refl n0); transitivity (eq_ind _ _ le_mn2 _ def_n2).
   2: reflexivity.
 generalize def_n2; revert le_mn1 le_mn2.
@@ -50,7 +49,7 @@ destruct le_mn1; intros le_mn2; destruct le_mn2.
   now destruct (Nat.nle_succ_diag_l _ le_mn0).
 + intros def_n0; generalize le_mn1; rewrite def_n0; intros le_mn0.
   now destruct (Nat.nle_succ_diag_l _ le_mn0).
-+ intros def_n0; injection def_n0; intros ->.
++ intros def_n0. injection def_n0 as ->.
   rewrite (UIP_nat _ _ def_n0 eq_refl); simpl.
   assert (H : le_mn1 = le_mn2).
     now apply IHn0.
diff --git a/theories/Arith/Plus.v b/theories/Arith/Plus.v
index 3b823da6..600e5e51 100644
--- a/theories/Arith/Plus.v
+++ b/theories/Arith/Plus.v
@@ -177,12 +177,12 @@ Proof (succ_plus_discr n 3).
 
 (** * Compatibility Hints *)
 
-Hint Immediate plus_comm : arith v62.
-Hint Resolve plus_assoc plus_assoc_reverse : arith v62.
-Hint Resolve plus_le_compat_l plus_le_compat_r : arith v62.
-Hint Resolve le_plus_l le_plus_r le_plus_trans : arith v62.
-Hint Immediate lt_plus_trans : arith v62.
-Hint Resolve plus_lt_compat_l plus_lt_compat_r : arith v62.
+Hint Immediate plus_comm : arith.
+Hint Resolve plus_assoc plus_assoc_reverse : arith.
+Hint Resolve plus_le_compat_l plus_le_compat_r : arith.
+Hint Resolve le_plus_l le_plus_r le_plus_trans : arith.
+Hint Immediate lt_plus_trans : arith.
+Hint Resolve plus_lt_compat_l plus_lt_compat_r : arith.
 
 (** For compatibility, we "Require" the same files as before *)
 
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 721ab693..06096c66 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -39,13 +39,13 @@ Lemma diff_true_false : true <> false.
 Proof.
   discriminate.
 Qed.
-Hint Resolve diff_true_false : bool v62.
+Hint Resolve diff_true_false : bool.
 
 Lemma diff_false_true : false <> true.
 Proof.
   discriminate.
 Qed.
-Hint Resolve diff_false_true : bool v62.
+Hint Resolve diff_false_true : bool.
 Hint Extern 1 (false <> true) => exact diff_false_true.
 
 Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False.
@@ -82,7 +82,7 @@ Definition leb (b1 b2:bool) :=
     | true => b2 = true
     | false => True
   end.
-Hint Unfold leb: bool v62.
+Hint Unfold leb: bool.
 
 Lemma leb_implb : forall b1 b2, leb b1 b2 <-> implb b1 b2 = true.
 Proof.
@@ -242,14 +242,14 @@ Lemma orb_true_intro :
 Proof.
  intros; apply orb_true_iff; trivial.
 Qed.
-Hint Resolve orb_true_intro: bool v62.
+Hint Resolve orb_true_intro: bool.
 
 Lemma orb_false_intro :
   forall b1 b2:bool, b1 = false -> b2 = false -> b1 || b2 = false.
 Proof.
  intros. subst. reflexivity.
 Qed.
-Hint Resolve orb_false_intro: bool v62.
+Hint Resolve orb_false_intro: bool.
 
 Lemma orb_false_elim :
   forall b1 b2:bool, b1 || b2 = false -> b1 = false /\ b2 = false.
@@ -268,7 +268,7 @@ Lemma orb_true_r : forall b:bool, b || true = true.
 Proof.
   destr_bool.
 Qed.
-Hint Resolve orb_true_r: bool v62.
+Hint Resolve orb_true_r: bool.
 
 Lemma orb_true_l : forall b:bool, true || b = true.
 Proof.
@@ -284,13 +284,13 @@ Lemma orb_false_r : forall b:bool, b || false = b.
 Proof.
   destr_bool.
 Qed.
-Hint Resolve orb_false_r: bool v62.
+Hint Resolve orb_false_r: bool.
 
 Lemma orb_false_l : forall b:bool, false || b = b.
 Proof.
   destr_bool.
 Qed.
-Hint Resolve orb_false_l: bool v62.
+Hint Resolve orb_false_l: bool.
 
 Notation orb_b_false := orb_false_r (only parsing).
 Notation orb_false_b := orb_false_l (only parsing).
@@ -301,7 +301,7 @@ Lemma orb_negb_r : forall b:bool, b || negb b = true.
 Proof.
   destr_bool.
 Qed.
-Hint Resolve orb_negb_r: bool v62.
+Hint Resolve orb_negb_r: bool.
 
 Notation orb_neg_b := orb_negb_r (only parsing).
 
@@ -318,7 +318,7 @@ Lemma orb_assoc : forall b1 b2 b3:bool, b1 || (b2 || b3) = b1 || b2 || b3.
 Proof.
   destr_bool.
 Qed.
-Hint Resolve orb_comm orb_assoc: bool v62.
+Hint Resolve orb_comm orb_assoc: bool.
 
 (*******************************)
 (** * Properties of [andb]     *)
@@ -392,7 +392,7 @@ Lemma andb_false_elim :
 Proof.
   destruct b1; simpl; auto.
 Defined.
-Hint Resolve andb_false_elim: bool v62.
+Hint Resolve andb_false_elim: bool.
 
 (** Complementation *)
 
@@ -400,7 +400,7 @@ Lemma andb_negb_r : forall b:bool, b && negb b = false.
 Proof.
   destr_bool.
 Qed.
-Hint Resolve andb_negb_r: bool v62.
+Hint Resolve andb_negb_r: bool.
 
 Notation andb_neg_b := andb_negb_r (only parsing).
 
@@ -418,7 +418,7 @@ Proof.
   destr_bool.
 Qed.
 
-Hint Resolve andb_comm andb_assoc: bool v62.
+Hint Resolve andb_comm andb_assoc: bool.
 
 (*******************************************)
 (** * Properties mixing [andb] and [orb] *)
@@ -688,7 +688,7 @@ Lemma andb_prop_intro :
 Proof.
   destr_bool; tauto.
 Qed.
-Hint Resolve andb_prop_intro: bool v62.
+Hint Resolve andb_prop_intro: bool.
 
 Notation andb_true_intro2 :=
   (fun b1 b2 H1 H2 => andb_prop_intro b1 b2 (conj H1 H2))
@@ -699,7 +699,7 @@ Lemma andb_prop_elim :
 Proof.
   destr_bool; auto.
 Qed.
-Hint Resolve andb_prop_elim: bool v62.
+Hint Resolve andb_prop_elim: bool.
 
 Notation andb_prop2 := andb_prop_elim (only parsing).
 
diff --git a/theories/Bool/IfProp.v b/theories/Bool/IfProp.v
index 11f3d1d6..4257b4bc 100644
--- a/theories/Bool/IfProp.v
+++ b/theories/Bool/IfProp.v
@@ -12,7 +12,7 @@ Inductive IfProp (A B:Prop) : bool -> Prop :=
   | Iftrue : A -> IfProp A B true
   | Iffalse : B -> IfProp A B false.
 
-Hint Resolve Iftrue Iffalse: bool v62.
+Hint Resolve Iftrue Iffalse: bool.
 
 Lemma Iftrue_inv : forall (A B:Prop) (b:bool), IfProp A B b -> b = true -> A.
 destruct 1; intros; auto with bool.
diff --git a/theories/Classes/CMorphisms.v b/theories/Classes/CMorphisms.v
index c41eb2fa..1cfca416 100644
--- a/theories/Classes/CMorphisms.v
+++ b/theories/Classes/CMorphisms.v
@@ -452,7 +452,7 @@ Ltac partial_application_tactic :=
   let rec do_partial_apps H m cont := 
     match m with
       | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; 
-        [(do_partial_apps H m' ltac:idtac)|clear H]
+        [(do_partial_apps H m' ltac:(idtac))|clear H]
       | _ => cont
     end
   in
@@ -527,7 +527,7 @@ Hint Extern 7 (@Proper _ _ _) => proper_reflexive
 Section Normalize.
   Context (A : Type).
 
-  Class Normalizes (m : crelation A) (m' : crelation A) : Prop :=
+  Class Normalizes (m : crelation A) (m' : crelation A) :=
     normalizes : relation_equivalence m m'.
   
   (** Current strategy: add [flip] everywhere and reduce using [subrelation]
diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v
index c4588947..80b0b7e4 100644
--- a/theories/Classes/Equivalence.v
+++ b/theories/Classes/Equivalence.v
@@ -49,11 +49,11 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope.
 
 (** Shortcuts to make proof search easier. *)
 
-Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv.
+Program Instance equiv_reflexive `(sa : Equivalence A) : Reflexive equiv | 1.
 
-Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv.
+Program Instance equiv_symmetric `(sa : Equivalence A) : Symmetric equiv | 1.
 
-Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv.
+Program Instance equiv_transitive `(sa : Equivalence A) : Transitive equiv | 1.
 
   Next Obligation.
   Proof. intros A R sa x y z Hxy Hyz.
@@ -123,7 +123,7 @@ Section Respecting.
 
 End Respecting.
 
-(** The default equivalence on function spaces, with higher-priority than [eq]. *)
+(** The default equivalence on function spaces, with higher priority than [eq]. *)
 
 Instance pointwise_reflexive {A} `(reflb : Reflexive B eqB) :
   Reflexive (pointwise_relation A eqB) | 9.
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index 8d942d90..06511ace 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -465,12 +465,12 @@ Ltac partial_application_tactic :=
   let rec do_partial_apps H m cont := 
     match m with
       | ?m' ?x => class_apply @Reflexive_partial_app_morphism ; 
-        [(do_partial_apps H m' ltac:idtac)|clear H]
+        [(do_partial_apps H m' ltac:(idtac))|clear H]
       | _ => cont
     end
   in
   let rec do_partial H ar m := 
-    match ar with
+    lazymatch ar with
       | 0%nat => do_partial_apps H m ltac:(fail 1)
       | S ?n' =>
         match m with
@@ -483,7 +483,7 @@ Ltac partial_application_tactic :=
      let n := fresh in evar (n:nat) ;
      let v := eval compute in n in clear n ;
       let H := fresh in
-        assert(H:Params m' v) by typeclasses eauto ;
+        assert(H:Params m' v) by (subst m'; once typeclasses eauto) ;
           let v' := eval compute in v in subst m';
             (sk H v' || fail 1))
     || fk
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index cbde5f9a..8d1c4982 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -43,6 +43,9 @@ Generalizable Variables A B RA RB Ri Ro f.
 Definition RelCompFun {A} {B : Type}(R:relation B)(f:A->B) : relation A :=
  fun a a' => R (f a) (f a').
 
+(** Instances on RelCompFun must match syntactically *)
+Typeclasses Opaque RelCompFun. 
+
 Infix "@@" := RelCompFun (at level 30, right associativity) : signature_scope.
 
 Notation "R @@1" := (R @@ Fst)%signature (at level 30) : signature_scope.
@@ -65,6 +68,8 @@ Instance snd_measure : @Measure (A * B) B Snd.
 Definition RelProd {A : Type} {B : Type} (RA:relation A)(RB:relation B) : relation (A*B) :=
  relation_conjunction (@RelCompFun (A * B) A RA fst) (RB @@2).
 
+Typeclasses Opaque RelProd.
+
 Infix "*" := RelProd : signature_scope.
 
 Section RelCompFun_Instances.
diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v
index 145d451f..190397ae 100644
--- a/theories/Classes/SetoidTactics.v
+++ b/theories/Classes/SetoidTactics.v
@@ -77,23 +77,23 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "by" tactic3(t) :=
-  setoidreplace (default_relation x y) ltac:t.
+  setoidreplace (default_relation x y) ltac:(t).
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "at" int_or_var_list(o)
   "by" tactic3(t) :=
-  setoidreplaceat (default_relation x y) ltac:t o.
+  setoidreplaceat (default_relation x y) ltac:(t) o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "in" hyp(id)
   "by" tactic3(t) :=
-  setoidreplacein (default_relation x y) id ltac:t.
+  setoidreplacein (default_relation x y) id ltac:(t).
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "in" hyp(id)
   "at" int_or_var_list(o)
   "by" tactic3(t) :=
-  setoidreplaceinat (default_relation x y) id ltac:t o.
+  setoidreplaceinat (default_relation x y) id ltac:(t) o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel) :=
@@ -107,13 +107,13 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "by" tactic3(t) :=
-  setoidreplace (rel x y) ltac:t.
+  setoidreplace (rel x y) ltac:(t).
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "at" int_or_var_list(o)
   "by" tactic3(t) :=
-  setoidreplaceat (rel x y) ltac:t o.
+  setoidreplaceat (rel x y) ltac:(t) o.
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
@@ -130,14 +130,14 @@ Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "in" hyp(id)
   "by" tactic3(t) :=
-  setoidreplacein (rel x y) id ltac:t.
+  setoidreplacein (rel x y) id ltac:(t).
 
 Tactic Notation "setoid_replace" constr(x) "with" constr(y)
   "using" "relation" constr(rel)
   "in" hyp(id)
   "at" int_or_var_list(o)
   "by" tactic3(t) :=
-  setoidreplaceinat (rel x y) id ltac:t o.
+  setoidreplaceinat (rel x y) id ltac:(t) o.
 
 (** The [add_morphism_tactic] tactic is run at each [Add Morphism]
    command before giving the hand back to the user to discharge the
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 90083b00..a3e23f91 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -7,6 +7,10 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.4 *)
+
+(** Any compatibility changes to make future versions of Coq behave like Coq 8.5 are likely needed to make them behave like Coq 8.4. *)
+Require Export Coq.Compat.Coq85.
+
 (** See https://coq.inria.fr/bugs/show_bug.cgi?id=4319 for updates *)
 (** This is required in Coq 8.5 to use the [omega] tactic; in Coq 8.4, it's automatically available.  But ZArith_base puts infix ~ at level 7, and we don't want that, so we don't [Import] it. *)
 Require Coq.omega.Omega.
@@ -15,21 +19,31 @@ Ltac omega := Coq.omega.Omega.omega.
 (** The number of arguments given in [match] statements has changed from 8.4 to 8.5. *)
 Global Set Asymmetric Patterns.
 
+(** The automatic elimination schemes for records were dropped by default in 8.5.  This restores the default behavior of Coq 8.4. *)
+Global Set Nonrecursive Elimination Schemes.
+
 (** See bug 3545 *)
 Global Set Universal Lemma Under Conjunction.
 
-(** In 8.5, [refine] leaves over dependent subgoals. *)
-Tactic Notation "refine" uconstr(term) := refine term; shelve_unifiable.
+(** Feature introduced in 8.5, disabled by default and configurable since 8.6. *)
+Global Unset Refolding Reduction.
 
 (** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *)
-Ltac constructor_84 := constructor.
 Ltac constructor_84_n n := constructor n.
 Ltac constructor_84_tac tac := once (constructor; tac).
 
-Tactic Notation "constructor" := constructor_84.
+Tactic Notation "constructor" := Coq.Init.Notations.constructor.
 Tactic Notation "constructor" int_or_var(n) := constructor_84_n n.
 Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac.
 
+(** In 8.4, [econstructor (tac)] allowed backtracking across the use of [econstructor]; it has been subsumed by [econstructor; tac]. *)
+Ltac econstructor_84_n n := econstructor n.
+Ltac econstructor_84_tac tac := once (econstructor; tac).
+
+Tactic Notation "econstructor" := Coq.Init.Notations.econstructor.
+Tactic Notation "econstructor" int_or_var(n) := econstructor_84_n n.
+Tactic Notation "econstructor" "(" tactic(tac) ")" := econstructor_84_tac tac.
+
 (** Some tactic notations do not factor well with tactics; we add global parsing entries for some tactics that would otherwise be overwritten by custom variants. See https://coq.inria.fr/bugs/show_bug.cgi?id=4392. *)
 Tactic Notation "reflexivity" := reflexivity.
 Tactic Notation "assumption" := assumption.
@@ -45,29 +59,21 @@ Tactic Notation "left" := left.
 Tactic Notation "eleft" := eleft.
 Tactic Notation "right" := right.
 Tactic Notation "eright" := eright.
-Tactic Notation "constructor" := constructor.
-Tactic Notation "econstructor" := econstructor.
 Tactic Notation "symmetry" := symmetry.
 Tactic Notation "split" := split.
 Tactic Notation "esplit" := esplit.
 
-Global Set Regular Subst Tactic.
-
-(** Some names have changed in the standard library, so we add aliases. *)
-Require Coq.ZArith.Int.
-Module Export Coq.
-  Module Export ZArith.
-    Module Int.
-      Module Z_as_Int.
-        Include Coq.ZArith.Int.Z_as_Int.
-        (* FIXME: Should these get a (compat "8.4")?  Or be moved to Z_as_Int, probably? *)
-        Notation plus := Coq.ZArith.Int.Z_as_Int.add (only parsing).
-        Notation minus := Coq.ZArith.Int.Z_as_Int.sub (only parsing).
-        Notation mult := Coq.ZArith.Int.Z_as_Int.mul (only parsing).
-      End Z_as_Int.
-    End Int.
-  End ZArith.
-End Coq.
-
 (** Many things now import [PeanoNat] rather than [NPeano], so we require it so that the old absolute names in [NPeano.Nat] are available. *)
 Require Coq.Numbers.Natural.Peano.NPeano.
+
+(** The following coercions were declared by default in Specif.v. *)
+Coercion sig_of_sig2 : sig2 >-> sig.
+Coercion sigT_of_sigT2 : sigT2 >-> sigT.
+Coercion sigT_of_sig : sig >-> sigT.
+Coercion sig_of_sigT : sigT >-> sig.
+Coercion sigT2_of_sig2 : sig2 >-> sigT2.
+Coercion sig2_of_sigT2 : sigT2 >-> sig2.
+
+(** In 8.4, the statement of admitted lemmas did not depend on the section
+    variables. *)
+Unset Keep Admitted Variables.
diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v
index 6e2b3564..64ba6b1e 100644
--- a/theories/Compat/Coq85.v
+++ b/theories/Compat/Coq85.v
@@ -7,3 +7,30 @@
 (************************************************************************)
 
 (** Compatibility file for making Coq act similar to Coq v8.5 *)
+
+(** Any compatibility changes to make future versions of Coq behave like Coq 8.6
+    are likely needed to make them behave like Coq 8.5. *)
+Require Export Coq.Compat.Coq86.
+
+(** We use some deprecated options in this file, so we disable the
+    corresponding warning, to silence the build of this file. *)
+Local Set Warnings "-deprecated-option".
+
+(* In 8.5, "intros [|]", taken e.g. on a goal "A\/B->C", does not
+   behave as "intros [H|H]" but leave instead hypotheses quantified in
+   the goal, here producing subgoals A->C and B->C. *)
+
+Global Unset Bracketing Last Introduction Pattern.
+Global Unset Regular Subst Tactic.
+Global Unset Structural Injection.
+Global Unset Shrink Abstract.
+Global Unset Shrink Obligations.
+Global Set Refolding Reduction.
+
+(** The resolution algorithm for type classes has changed. *)
+Global Set Typeclasses Legacy Resolution.
+Global Set Typeclasses Limit Intros.
+Global Unset Typeclasses Filtered Unification.
+
+(** Allow silently letting unification constraints float after a "." *)
+Global Unset Solve Unification Constraints.
diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq86.v
new file mode 100644
index 00000000..6952fdf1
--- /dev/null
+++ b/theories/Compat/Coq86.v
@@ -0,0 +1,9 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** Compatibility file for making Coq act similar to Coq v8.6 *)
\ No newline at end of file
diff --git a/theories/Compat/vo.itarget b/theories/Compat/vo.itarget
index 43b19700..7ffb86eb 100644
--- a/theories/Compat/vo.itarget
+++ b/theories/Compat/vo.itarget
@@ -1,3 +1,4 @@
 AdmitAxiom.vo
 Coq84.vo
 Coq85.vo
+Coq86.vo
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index eaeb2914..3c5690a7 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -24,6 +24,8 @@ Hint Extern 1 (Equivalence _) => constructor; congruence.
 
 Module WFacts_fun (E:DecidableType)(Import M:WSfun E).
 
+Notation option_map := option_map (compat "8.4").
+
 Notation eq_dec := E.eq_dec.
 Definition eqb x y := if eq_dec x y then true else false.
 
@@ -1986,7 +1988,7 @@ Module OrdProperties (M:S).
   simpl; intros; try discriminate.
   intros.
   destruct a; destruct l; simpl in *.
-  injection H; clear H; intros; subst.
+  injection H as -> ->.
   inversion_clear H1.
   red in H; simpl in *; intuition.
   elim H0; eauto.
@@ -2050,10 +2052,10 @@ Module OrdProperties (M:S).
   generalize (elements_3 m).
   destruct (elements m).
   try discriminate.
-  destruct p; injection H; intros; subst.
-  inversion_clear H1.
+  destruct p; injection H as -> ->; intros H4.
+  inversion_clear H1 as [? ? H2|? ? H2].
   red in H2; destruct H2; simpl in *; ME.order.
-  inversion_clear H4.
+  inversion_clear H4. rename H1 into H3.
   rewrite (@InfA_alt _ eqke) in H3; eauto with *.
   apply (H3 (y,x0)); auto.
   Qed.
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 13cb559b..5acdb7eb 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -8,7 +8,7 @@
 
 (** * Finite map library *)
 
-(** This file proposes an implementation of the non-dependant interface
+(** This file proposes an implementation of the non-dependent interface
  [FMapInterface.S] using lists of pairs ordered (increasing) with respect to
  left projection. *)
 
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index 9e59f0c5..b1c0fdaa 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -274,8 +274,8 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
         rewrite append_assoc_1; apply in_or_app; right; apply in_cons;
           apply IHm2; auto.
         rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto.
-        rewrite append_neutral_r; apply in_or_app; injection H;
-          intro EQ; rewrite EQ; right; apply in_eq.
+        rewrite append_neutral_r; apply in_or_app; injection H as ->;
+          right; apply in_eq.
         rewrite append_assoc_1; apply in_or_app; right; apply IHm2; auto.
         rewrite append_assoc_0; apply in_or_app; left; apply IHm1; auto.
         congruence.
@@ -315,7 +315,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
          apply in_or_app.
         left; apply IHm1; auto.
         right; destruct (in_inv H0).
-         injection H1; intros Eq1 Eq2; rewrite Eq1; rewrite Eq2; apply in_eq.
+         injection H1 as -> ->; apply in_eq.
          apply in_cons; apply IHm2; auto.
         left; apply IHm1; auto.
         right; apply IHm2; auto.
@@ -346,7 +346,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
          apply in_or_app.
         left; apply IHm1; auto.
         right; destruct (in_inv H0).
-         injection H1; intros Eq1 Eq2; rewrite Eq1; rewrite Eq2; apply in_eq.
+         injection H1 as -> ->; apply in_eq.
          apply in_cons; apply IHm2; auto.
         left; apply IHm1; auto.
         right; apply IHm2; auto.
@@ -689,7 +689,7 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   destruct y2; destruct y0; compute in Hy2; destruct Hy2; subst.
   red; red; simpl.
   destruct H0.
-  injection H0; clear H0; intros _ H0; subst.
+  injection H0 as H0 _; subst.
   eapply xelements_bits_lt_1; eauto.
   apply E.bits_lt_trans with p.
   eapply xelements_bits_lt_1; eauto.
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 0f11dd7a..130cbee8 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -8,7 +8,7 @@
 
 (** * Finite map library *)
 
-(** This file proposes an implementation of the non-dependant interface
+(** This file proposes an implementation of the non-dependent interface
  [FMapInterface.WS] using lists of pairs, unordered but without redundancy. *)
 
 Require Import FMapInterface.
diff --git a/theories/FSets/FSetDecide.v b/theories/FSets/FSetDecide.v
index ad067eb3..1db6a71e 100644
--- a/theories/FSets/FSetDecide.v
+++ b/theories/FSets/FSetDecide.v
@@ -357,17 +357,8 @@ the above form:
         | _ => idtac
       end.
 
-    (** [if t then t1 else t2] executes [t] and, if it does not
-        fail, then [t1] will be applied to all subgoals
-        produced.  If [t] fails, then [t2] is executed. *)
-    Tactic Notation
-      "if" tactic(t)
-      "then" tactic(t1)
-      "else" tactic(t2) :=
-      first [ t; first [ t1 | fail 2 ] | t2 ].
-
     Ltac abstract_term t :=
-      if (is_var t) then fail "no need to abstract a variable"
+      tryif (is_var t) then fail "no need to abstract a variable"
       else (let x := fresh "x" in set (x := t) in *; try clearbody x).
 
     Ltac abstract_elements :=
@@ -478,11 +469,11 @@ the above form:
       repeat (
         match goal with
         | H : context [ @Logic.eq ?T ?x ?y ] |- _ =>
-          if (change T with E.t in H) then fail
-          else if (change T with t in H) then fail
+          tryif (change T with E.t in H) then fail
+          else tryif (change T with t in H) then fail
           else clear H
         | H : ?P |- _ =>
-          if prop (FSet_Prop P) holds by
+          tryif prop (FSet_Prop P) holds by
             (auto 100 with FSet_Prop)
           then fail
           else clear H
@@ -747,7 +738,7 @@ the above form:
     | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
       contradict H; fsetdec_body
     | H: ?P -> False |- ?Q -> False =>
-      if prop (FSet_elt_Prop P) holds by
+      tryif prop (FSet_elt_Prop P) holds by
         (auto 100 with FSet_Prop)
       then (contradict H; fsetdec_body)
       else fsetdec_body
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index 1f36306c..9c3ec71a 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -8,7 +8,7 @@
 
 (** * Finite sets library *)
 
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
     interface [FSetInterface.S] using strictly ordered list. *)
 
 Require Export FSetInterface.
diff --git a/theories/FSets/FSetPositive.v b/theories/FSets/FSetPositive.v
index 7398c6d6..507f1cda 100644
--- a/theories/FSets/FSetPositive.v
+++ b/theories/FSets/FSetPositive.v
@@ -1007,10 +1007,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       destruct o.
         intros x H. injection H; intros; subst. reflexivity.
         revert IHl. case choose.
-          intros p Hp x H. injection H; intros; subst; clear H. apply Hp.
+          intros p Hp x H. injection H as <-. apply Hp.
            reflexivity.
           intros _ x. revert IHr. case choose.
-            intros p Hp H. injection H; intros; subst; clear H. apply Hp.
+            intros p Hp H. injection H as <-. apply Hp.
             reflexivity.
             intros. discriminate.
   Qed.
@@ -1066,11 +1066,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
    induction s as [| l IHl o r IHr]; simpl.
      intros. discriminate.
      intros x. destruct (min_elt l); intros.
-       injection H. intros <-. apply IHl. reflexivity.
+       injection H as <-. apply IHl. reflexivity.
        destruct o; simpl.
-         injection H. intros <-. reflexivity.
+         injection H as <-. reflexivity.
          destruct (min_elt r); simpl in *.
-           injection H. intros <-. apply IHr. reflexivity.
+           injection H as <-. apply IHr. reflexivity.
            discriminate.
   Qed.
 
@@ -1094,15 +1094,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     induction s as [|l IHl o r IHr]; intros x y H H'.
       discriminate.
       simpl in H. case_eq (min_elt l).
-        intros p Hp. rewrite Hp in H. injection H; intros <-.
+        intros p Hp. rewrite Hp in H. injection H as <-.
         destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial.
         intro Hp; rewrite Hp in H. apply min_elt_3 in Hp.
         destruct o.
-          injection H. intros <- Hl. clear H.
+          injection H as <-. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (min_elt r).
-            injection H. intros <-. clear H.
+            injection H as <-.
             destruct y as [z|z|].
               apply (IHr e z); trivial.
               elim (Hp _ H').
@@ -1119,11 +1119,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
    induction s as [| l IHl o r IHr]; simpl.
      intros. discriminate.
      intros x. destruct (max_elt r); intros.
-       injection H. intros <-. apply IHr. reflexivity.
+       injection H as <-. apply IHr. reflexivity.
        destruct o; simpl.
-         injection H. intros <-. reflexivity.
+         injection H as <-. reflexivity.
          destruct (max_elt l); simpl in *.
-           injection H. intros <-. apply IHl. reflexivity.
+           injection H as <-. apply IHl. reflexivity.
            discriminate.
   Qed.
 
@@ -1147,15 +1147,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     induction s as [|l IHl o r IHr]; intros x y H H'.
       discriminate.
       simpl in H. case_eq (max_elt r).
-        intros p Hp. rewrite Hp in H. injection H; intros <-.
+        intros p Hp. rewrite Hp in H. injection H as <-.
         destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial.
         intro Hp; rewrite Hp in H. apply max_elt_3 in Hp.
         destruct o.
-          injection H. intros <- Hl. clear H.
+          injection H as <-. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (max_elt l).
-            injection H. intros <-. clear H.
+            injection H as <-.
             destruct y as [z|z|].
               elim (Hp _ H').
               apply (IHl e z); trivial.
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 2ea32e97..9dbea884 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -8,7 +8,7 @@
 
 (** * Finite sets library *)
 
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
     interface [FSetInterface.WS] using lists without redundancy. *)
 
 Require Import FSetInterface.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 4850c9ca..ddaf08bf 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -151,6 +151,7 @@ Inductive option (A:Type) : Type :=
   | Some : A -> option A
   | None : option A.
 
+Arguments Some {A} a.
 Arguments None {A}.
 
 Definition option_map (A B:Type) (f:A->B) (o : option A) : option B :=
@@ -225,6 +226,7 @@ Inductive list (A : Type) : Type :=
  | cons : A -> list A -> list A.
 
 Arguments nil {A}.
+Arguments cons {A} a l.
 Infix "::" := cons (at level 60, right associativity) : list_scope.
 Delimit Scope list_scope with list.
 Bind Scope list_scope with list.
diff --git a/theories/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 4a5f2ad6..4536dfc0 100644
--- a/theories/Init/Logic_Type.v
+++ b/theories/Init/Logic_Type.v
@@ -64,7 +64,7 @@ Definition identity_rect_r :
  intros A x P H y H0; case identity_sym with (1 := H0); trivial.
 Defined.
 
-Hint Immediate identity_sym not_identity_sym: core v62.
+Hint Immediate identity_sym not_identity_sym: core.
 
 Notation refl_id := identity_refl (compat "8.3").
 Notation sym_id := identity_sym (compat "8.3").
diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v
index ab6bf472..48fbe079 100644
--- a/theories/Init/Notations.v
+++ b/theories/Init/Notations.v
@@ -76,17 +76,21 @@ Reserved Notation "{ x : A  & P }" (at level 0, x at level 99).
 Reserved Notation "{ x : A  & P  & Q }" (at level 0, x at level 99).
 
 Delimit Scope type_scope with type.
+Delimit Scope function_scope with function.
 Delimit Scope core_scope with core.
 
+Bind Scope type_scope with Sortclass.
+Bind Scope function_scope with Funclass.
+
 Open Scope core_scope.
+Open Scope function_scope.
 Open Scope type_scope.
 
 (** ML Tactic Notations *)
 
 Declare ML Module "coretactics".
 Declare ML Module "extratactics".
-Declare ML Module "eauto".
+Declare ML Module "g_auto".
 Declare ML Module "g_class".
 Declare ML Module "g_eqdecide".
 Declare ML Module "g_rewrite".
-Declare ML Module "tauto".
diff --git a/theories/Init/Peano.v b/theories/Init/Peano.v
index 3749baf6..6c4a6350 100644
--- a/theories/Init/Peano.v
+++ b/theories/Init/Peano.v
@@ -33,7 +33,6 @@ Open Scope nat_scope.
 Definition eq_S := f_equal S.
 Definition f_equal_nat := f_equal (A:=nat).
 
-Hint Resolve eq_S: v62.
 Hint Resolve f_equal_nat: core.
 
 (** The predecessor function *)
@@ -41,7 +40,6 @@ Hint Resolve f_equal_nat: core.
 Notation pred := Nat.pred (compat "8.4").
 
 Definition f_equal_pred := f_equal pred.
-Hint Resolve f_equal_pred: v62.
 
 Theorem pred_Sn : forall n:nat, n = pred (S n).
 Proof.
@@ -85,7 +83,6 @@ Notation plus := Nat.add (compat "8.4").
 Infix "+" := Nat.add : nat_scope.
 
 Definition f_equal2_plus := f_equal2 plus.
-Hint Resolve f_equal2_plus: v62.
 Definition f_equal2_nat := f_equal2 (A1:=nat) (A2:=nat). 
 Hint Resolve f_equal2_nat: core.
 
diff --git a/theories/Init/Prelude.v b/theories/Init/Prelude.v
index 04a263ad..03f2328d 100644
--- a/theories/Init/Prelude.v
+++ b/theories/Init/Prelude.v
@@ -15,6 +15,7 @@ Require Coq.Init.Nat.
 Require Export Peano.
 Require Export Coq.Init.Wf.
 Require Export Coq.Init.Tactics.
+Require Export Coq.Init.Tauto.
 (* Initially available plugins
    (+ nat_syntax_plugin loaded in Datatypes) *)
 Declare ML Module "extraction_plugin".
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 6c022185..9fc00e80 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -9,6 +9,7 @@
 (** Basic specifications : sets that may contain logical information *)
 
 Set Implicit Arguments.
+Set Reversible Pattern Implicit.
 
 Require Import Notations.
 Require Import Datatypes.
@@ -298,7 +299,7 @@ Proof.
   apply (h2 h1).
 Defined.
 
-Hint Resolve left right inleft inright: core v62.
+Hint Resolve left right inleft inright: core.
 Hint Resolve exist exist2 existT existT2: core.
 
 (* Compatibility *)
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index 59fdbb42..5d1e87ae 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -55,12 +55,6 @@ Ltac contradict H :=
    | _ => (elim H;fail) || pos H
   end.
 
-(* Transforming a negative goal [ H:~A |- ~B ] into a positive one [ B |- A ]*)
-
-Ltac swap H :=
-  idtac "swap is OBSOLETE: use contradict instead.";
-  intro; apply H; clear H.
-
 (* To contradict an hypothesis without copying its type. *)
 
 Ltac absurd_hyp H :=
@@ -79,7 +73,7 @@ Ltac case_eq x := generalize (eq_refl x); pattern x at -1; case x.
 
 (* use either discriminate or injection on a hypothesis *)
 
-Ltac destr_eq H := discriminate H || (try (injection H; clear H; intro H)).
+Ltac destr_eq H := discriminate H || (try (injection H as H)).
 
 (* Similar variants of destruct *)
 
diff --git a/theories/Init/Tauto.v b/theories/Init/Tauto.v
new file mode 100644
index 00000000..1e409607
--- /dev/null
+++ b/theories/Init/Tauto.v
@@ -0,0 +1,101 @@
+Require Import Notations.
+Require Import Datatypes.
+Require Import Logic.
+
+Local Declare ML Module "tauto".
+
+Local Ltac not_dep_intros :=
+  repeat match goal with
+  | |- (forall (_: ?X1), ?X2) => intro
+  | |- (Coq.Init.Logic.not _) => unfold Coq.Init.Logic.not at 1; intro
+  end.
+
+Local Ltac axioms flags :=
+  match reverse goal with
+    | |- ?X1 => is_unit_or_eq flags X1; constructor 1
+    | _:?X1 |- _ => is_empty flags X1; elimtype X1; assumption
+    | _:?X1 |- ?X1 => assumption
+  end.
+
+Local Ltac simplif flags :=
+  not_dep_intros;
+  repeat
+     (match reverse goal with
+      | id: ?X1 |- _ => is_conj flags X1; elim id; do 2 intro; clear id
+      | id: (Coq.Init.Logic.iff _ _) |- _ => elim id; do 2 intro; clear id
+      | id: (Coq.Init.Logic.not _) |- _ => red in id
+      | id: ?X1 |- _ => is_disj flags X1; elim id; intro; clear id
+      | id0: (forall (_: ?X1), ?X2), id1: ?X1|- _ =>
+    (* generalize (id0 id1); intro; clear id0 does not work
+       (see Marco Maggiesi's bug PR#301)
+    so we instead use Assert and exact. *)
+    assert X2; [exact (id0 id1) | clear id0]
+      | id: forall (_ : ?X1), ?X2|- _ =>
+        is_unit_or_eq flags X1; cut X2;
+    [ intro; clear id
+    | (* id : forall (_: ?X1), ?X2 |- ?X2 *)
+      cut X1; [exact id| constructor 1; fail]
+    ]
+      | id: forall (_ : ?X1), ?X2|- _ =>
+        flatten_contravariant_conj flags X1 X2 id
+  (* moved from "id:(?A/\?B)->?X2|-" to "?A->?B->?X2|-" *)
+      | id: forall (_: Coq.Init.Logic.iff ?X1 ?X2), ?X3|- _ =>
+        assert (forall (_: forall _:X1, X2), forall (_: forall _: X2, X1), X3)
+    by (do 2 intro; apply id; split; assumption);
+          clear id
+      | id: forall (_:?X1), ?X2|- _ =>
+        flatten_contravariant_disj flags X1 X2 id
+  (* moved from "id:(?A\/?B)->?X2|-" to "?A->?X2,?B->?X2|-" *)
+      | |- ?X1 => is_conj flags X1; split
+      | |- (Coq.Init.Logic.iff _ _) => split
+      | |- (Coq.Init.Logic.not _) => red
+      end;
+      not_dep_intros).
+
+Local Ltac tauto_intuit flags t_reduce t_solver :=
+ let rec t_tauto_intuit :=
+ (simplif flags; axioms flags
+ || match reverse goal with
+    | id:forall(_: forall (_: ?X1), ?X2), ?X3|- _ =>
+  cut X3;
+    [ intro; clear id; t_tauto_intuit
+    | cut (forall (_: X1), X2);
+	[ exact id
+	| generalize (fun y:X2 => id (fun x:X1 => y)); intro; clear id;
+	  solve [ t_tauto_intuit ]]]
+    | id:forall (_:not ?X1), ?X3|- _ =>
+  cut X3;
+    [ intro; clear id; t_tauto_intuit
+    | cut (not X1); [ exact id | clear id; intro; solve [t_tauto_intuit ]]]
+    | |- ?X1 =>
+        is_disj flags X1; solve [left;t_tauto_intuit | right;t_tauto_intuit]
+    end
+  ||
+  (* NB: [|- _ -> _] matches any product *)
+  match goal with | |- forall (_ : _),  _ => intro; t_tauto_intuit
+  |  |- _  => t_reduce;t_solver
+  end
+  ||
+  t_solver
+ ) in t_tauto_intuit.
+
+Local Ltac intuition_gen flags solver := tauto_intuit flags reduction_not_iff solver.
+Local Ltac tauto_intuitionistic flags := intuition_gen flags fail || fail "tauto failed".
+Local Ltac tauto_classical flags :=
+  (apply_nnpp || fail "tauto failed"); (tauto_intuitionistic flags || fail "Classical tauto failed").
+Local Ltac tauto_gen flags := tauto_intuitionistic flags || tauto_classical flags.
+
+Ltac tauto := with_uniform_flags ltac:(fun flags => tauto_gen flags).
+Ltac dtauto := with_power_flags ltac:(fun flags => tauto_gen flags).
+
+Ltac intuition := with_uniform_flags ltac:(fun flags => intuition_gen flags ltac:(auto with *)).
+Local Ltac intuition_then tac := with_uniform_flags ltac:(fun flags => intuition_gen flags tac).
+
+Ltac dintuition := with_power_flags ltac:(fun flags => intuition_gen flags ltac:(auto with *)).
+Local Ltac dintuition_then tac := with_power_flags ltac:(fun flags => intuition_gen flags tac).
+
+Tactic Notation "intuition" := intuition.
+Tactic Notation "intuition" tactic(t) := intuition_then t.
+
+Tactic Notation "dintuition" := dintuition.
+Tactic Notation "dintuition" tactic(t) := dintuition_then t.
diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 985ecaf2..b5b17e5e 100644
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -34,7 +34,7 @@ Section Well_founded.
   destruct 1; trivial.
  Defined.
 
- Global Implicit Arguments Acc_inv [x y] [x].
+ Global Arguments Acc_inv [x] _ [y] _, [x] _ y _.
 
  (** A relation is well-founded if every element is accessible *)
 
diff --git a/theories/Init/vo.itarget b/theories/Init/vo.itarget
index cc62e66c..99877065 100644
--- a/theories/Init/vo.itarget
+++ b/theories/Init/vo.itarget
@@ -7,4 +7,5 @@ Prelude.vo
 Specif.vo
 Tactics.vo
 Wf.vo
-Nat.vo
\ No newline at end of file
+Nat.vo
+Tauto.vo
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index cc7586fe..30f1dec2 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -7,7 +7,7 @@
 (************************************************************************)
 
 Require Setoid.
-Require Import PeanoNat Le Gt Minus Bool.
+Require Import PeanoNat Le Gt Minus Bool Lt.
 
 Set Implicit Arguments.
 (* Set Universe Polymorphism. *)
@@ -21,12 +21,13 @@ Set Implicit Arguments.
 
 Open Scope list_scope.
 
-(** Standard notations for lists. 
+(** Standard notations for lists.
 In a special module to avoid conflicts. *)
 Module ListNotations.
-Notation " [ ] " := nil (format "[ ]") : list_scope.
-Notation " [ x ] " := (cons x nil) : list_scope.
-Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope.
+Notation "[ ]" := nil (format "[ ]") : list_scope.
+Notation "[ x ]" := (cons x nil) : list_scope.
+Notation "[ x ; y ; .. ; z ]" :=  (cons x (cons y .. (cons z nil) ..)) : list_scope.
+Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..) (compat "8.4") : list_scope.
 End ListNotations.
 
 Import ListNotations.
@@ -195,7 +196,7 @@ Section Facts.
   Qed.
 
   Theorem app_nil_r : forall l:list A, l ++ [] = l.
-  Proof. 
+  Proof.
     induction l; simpl; f_equal; auto.
   Qed.
 
@@ -248,8 +249,7 @@ Section Facts.
     generalize (app_nil_r l); intros E.
     rewrite -> E; auto.
     intros.
-    injection H.
-    intro.
+    injection H as H H0.
     assert ([] = l ++ a0 :: l0) by auto.
     apply app_cons_not_nil in H1 as [].
   Qed.
@@ -335,16 +335,16 @@ Section Facts.
     absurd (length (x1 :: l1 ++ l) <= length l).
     simpl; rewrite app_length; auto with arith.
     rewrite H; auto with arith.
-    injection H; clear H; intros; f_equal; eauto.
+    injection H as H H0; f_equal; eauto.
   Qed.
 
 End Facts.
 
-Hint Resolve app_assoc app_assoc_reverse: datatypes v62.
-Hint Resolve app_comm_cons app_cons_not_nil: datatypes v62.
-Hint Immediate app_eq_nil: datatypes v62.
-Hint Resolve app_eq_unit app_inj_tail: datatypes v62.
-Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes v62.
+Hint Resolve app_assoc app_assoc_reverse: datatypes.
+Hint Resolve app_comm_cons app_cons_not_nil: datatypes.
+Hint Immediate app_eq_nil: datatypes.
+Hint Resolve app_eq_unit app_inj_tail: datatypes.
+Hint Resolve in_eq in_cons in_inv in_nil in_app_or in_or_app: datatypes.
 
 
 
@@ -518,7 +518,7 @@ Section Elts.
   Proof.
     revert l.
     induction n as [|n IH]; intros [|x l] H; simpl in *; try easy.
-    - exists nil; exists l. injection H; clear H; intros; now subst.
+    - exists nil; exists l. now injection H as ->.
     - destruct (IH _ H) as (l1 & l2 & H1 & H2).
       exists (x::l1); exists l2; simpl; split; now f_equal.
   Qed.
@@ -1385,9 +1385,8 @@ End Fold_Right_Recursor.
     Lemma combine_split : forall (l:list A)(l':list B), length l = length l' ->
       split (combine l l') = (l,l').
     Proof.
-      induction l; destruct l'; simpl; intros; auto; try discriminate.
-      injection H; clear H; intros.
-      rewrite IHl; auto.
+      induction l, l'; simpl; trivial; try discriminate.
+      now intros [= ->%IHl].
     Qed.
 
     Lemma in_combine_l : forall (l:list A)(l':list B)(x:A)(y:B),
@@ -1471,7 +1470,7 @@ End Fold_Right_Recursor.
       destruct (in_app_or _ _ _ H); clear H.
       destruct (in_map_iff (fun y : B => (a, y)) l' (x,y)) as (H1,_).
       destruct (H1 H0) as (z,(H2,H3)); clear H0 H1.
-      injection H2; clear H2; intros; subst; intuition.
+      injection H2 as -> ->; intuition.
       intuition.
     Qed.
 
@@ -1545,7 +1544,7 @@ Section length_order.
 End length_order.
 
 Hint Resolve lel_refl lel_cons_cons lel_cons lel_nil lel_nil nil_cons:
-  datatypes v62.
+  datatypes.
 
 
 (******************************)
@@ -1614,7 +1613,7 @@ Section SetIncl.
 End SetIncl.
 
 Hint Resolve incl_refl incl_tl incl_tran incl_appl incl_appr incl_cons
-  incl_app: datatypes v62.
+  incl_app: datatypes.
 
 
 (**************************************)
@@ -1634,6 +1633,80 @@ Section Cutting.
 	       end
     end.
 
+  Lemma firstn_nil n: firstn n [] = [].
+  Proof. induction n; now simpl. Qed.
+
+  Lemma firstn_cons n a l: firstn (S n) (a::l) = a :: (firstn n l).
+  Proof. now simpl. Qed.
+
+  Lemma firstn_all l: firstn (length l) l = l.
+  Proof. induction l as [| ? ? H]; simpl; [reflexivity | now rewrite H]. Qed.
+
+  Lemma firstn_all2 n: forall (l:list A), (length l) <= n -> firstn n l = l.
+  Proof. induction n as [|k iHk].
+    - intro. inversion 1 as [H1|?].
+      rewrite (length_zero_iff_nil l) in H1. subst. now simpl.
+    - destruct l as [|x xs]; simpl.
+      * now reflexivity.
+      * simpl. intro H. apply Peano.le_S_n in H. f_equal. apply iHk, H.
+  Qed.
+
+  Lemma firstn_O l: firstn 0 l = [].
+  Proof. now simpl. Qed.
+
+  Lemma firstn_le_length n: forall l:list A, length (firstn n l) <= n.
+  Proof.
+    induction n as [|k iHk]; simpl; [auto | destruct l as [|x xs]; simpl].
+    - auto with arith.
+    - apply Peano.le_n_S, iHk.
+  Qed.
+
+  Lemma firstn_length_le: forall l:list A, forall n:nat,
+    n <= length l -> length (firstn n l) = n.
+  Proof. induction l as [|x xs Hrec].
+    - simpl. intros n H. apply le_n_0_eq in H. rewrite <- H. now simpl.
+    - destruct n.
+      * now simpl.
+      * simpl. intro H. apply le_S_n in H. now rewrite (Hrec n H).
+  Qed.
+
+  Lemma firstn_app n:
+    forall l1 l2,
+    firstn n (l1 ++ l2) = (firstn n l1) ++ (firstn (n - length l1) l2).
+  Proof. induction n as [|k iHk]; intros l1 l2.
+    - now simpl.
+    - destruct l1 as [|x xs].
+      * unfold firstn at 2, length. now rewrite 2!app_nil_l, <- minus_n_O.
+      * rewrite <- app_comm_cons. simpl. f_equal. apply iHk.
+  Qed.
+
+  Lemma firstn_app_2 n:
+    forall l1 l2,
+    firstn ((length l1) + n) (l1 ++ l2) = l1 ++ firstn n l2.
+  Proof. induction n as [| k iHk];intros l1 l2.
+    - unfold firstn at 2. rewrite <- plus_n_O, app_nil_r.
+      rewrite firstn_app. rewrite <- minus_diag_reverse.
+      unfold firstn at 2. rewrite app_nil_r. apply firstn_all.
+    - destruct l2 as [|x xs].
+      * simpl. rewrite app_nil_r. apply firstn_all2. auto with arith.
+      * rewrite firstn_app. assert (H0 : (length l1 + S k - length l1) = S k).
+        auto with arith.
+        rewrite H0, firstn_all2; [reflexivity | auto with arith].
+  Qed.
+
+  Lemma firstn_firstn:
+    forall l:list A,
+    forall i j : nat,
+    firstn i (firstn j l) = firstn (min i j) l.
+  Proof. induction l as [|x xs Hl].
+    - intros. simpl. now rewrite ?firstn_nil.
+    - destruct i.
+      * intro. now simpl.
+      * destruct j.
+        + now simpl.
+        + simpl. f_equal. apply Hl.
+  Qed.
+
   Fixpoint skipn (n:nat)(l:list A) : list A :=
     match n with
       | 0 => l
@@ -2292,7 +2365,7 @@ Notation rev_acc := rev_append (only parsing).
 Notation rev_acc_rev := rev_append_rev (only parsing).
 Notation AllS := Forall (only parsing). (* was formerly in TheoryList *)
 
-Hint Resolve app_nil_end : datatypes v62.
+Hint Resolve app_nil_end : datatypes.
 (* end hide *)
 
 Section Repeat.
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index fd0464fb..655d3940 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -48,7 +48,11 @@ Section first_definitions.
         end
     end.
 
-  (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing *)
+  (** If [a] belongs to [x], removes [a] from [x]. If not, does nothing.
+      Invariant: any element should occur at most once in [x], see for
+      instance [set_add]. We hence remove here only the first occurrence
+      of [a] in [x]. *)
+
   Fixpoint set_remove (a:A) (x:set) : set :=
     match x with
     | nil => empty_set
@@ -227,6 +231,68 @@ Section first_definitions.
     intros; elim (Aeq_dec a a0); intros; discriminate.
   Qed.
 
+  Lemma set_add_iff a b l : In a (set_add b l) <-> a = b \/ In a l.
+  Proof.
+  split. apply set_add_elim. apply set_add_intro.
+  Qed.
+
+  Lemma set_add_nodup a l : NoDup l -> NoDup (set_add a l).
+  Proof.
+   induction 1 as [|x l H H' IH]; simpl.
+   - constructor; [ tauto | constructor ].
+   - destruct (Aeq_dec a x) as [<-|Hax]; constructor; trivial.
+     rewrite set_add_iff. intuition.
+  Qed.
+
+  Lemma set_remove_1 (a b : A) (l : set) :
+    In a (set_remove b l) -> In a l.
+  Proof.
+    induction l as [|x xs Hrec].
+    - intros. auto.
+    - simpl. destruct (Aeq_dec b x).
+      * tauto.
+      * intro H. destruct H.
+        + rewrite H. apply in_eq.
+      + apply in_cons. apply Hrec. assumption.
+  Qed.
+
+  Lemma set_remove_2 (a b:A) (l : set) :
+    NoDup l -> In a (set_remove b l) -> a <> b.
+  Proof.
+    induction l as [|x l IH]; intro ND; simpl.
+    - tauto.
+    - inversion_clear ND.
+      destruct (Aeq_dec b x) as [<-|Hbx].
+      + congruence.
+      + destruct 1; subst; auto.
+  Qed.
+
+  Lemma set_remove_3 (a b : A) (l : set) :
+    In a l -> a <> b -> In a (set_remove b l).
+  Proof.
+    induction l as [|x xs Hrec].
+    - now simpl.
+    - simpl. destruct (Aeq_dec b x) as [<-|Hbx]; simpl; intuition.
+      congruence.
+  Qed.
+
+  Lemma set_remove_iff (a b : A) (l : set) :
+   NoDup l -> (In a (set_remove b l) <-> In a l /\ a <> b).
+  Proof.
+   split; try split.
+   - eapply set_remove_1; eauto.
+   - eapply set_remove_2; eauto.
+   - destruct 1; apply set_remove_3; auto.
+  Qed.
+
+  Lemma set_remove_nodup a l : NoDup l -> NoDup (set_remove a l).
+  Proof.
+   induction 1 as [|x l H H' IH]; simpl.
+   - constructor.
+   - destruct (Aeq_dec a x) as [<-|Hax]; trivial.
+     constructor; trivial.
+     rewrite set_remove_iff; trivial. intuition.
+  Qed.
 
   Lemma set_union_intro1 :
    forall (a:A) (x y:set), set_In a x -> set_In a (set_union x y).
@@ -264,18 +330,26 @@ Section first_definitions.
     tauto.
   Qed.
 
+  Lemma set_union_iff a l l': In a (set_union l l') <-> In a l \/ In a l'.
+  Proof.
+    split. apply set_union_elim. apply set_union_intro.
+  Qed.
+
+  Lemma set_union_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_union l l').
+  Proof.
+   induction 2 as [|x' l' ? ? IH]; simpl; trivial. now apply set_add_nodup.
+  Qed.
+
   Lemma set_union_emptyL :
    forall (a:A) (x:set), set_In a (set_union empty_set x) -> set_In a x.
     intros a x H; case (set_union_elim _ _ _ H); auto || contradiction.
   Qed.
 
-
   Lemma set_union_emptyR :
    forall (a:A) (x:set), set_In a (set_union x empty_set) -> set_In a x.
     intros a x H; case (set_union_elim _ _ _ H); auto || contradiction.
   Qed.
 
-
   Lemma set_inter_intro :
    forall (a:A) (x y:set),
      set_In a x -> set_In a y -> set_In a (set_inter x y).
@@ -326,6 +400,21 @@ Section first_definitions.
     eauto with datatypes.
   Qed.
 
+  Lemma set_inter_iff a l l' : In a (set_inter l l') <-> In a l /\ In a l'.
+  Proof.
+    split.
+    - apply set_inter_elim.
+    - destruct 1. now apply set_inter_intro.
+  Qed.
+
+  Lemma set_inter_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_inter l l').
+  Proof.
+   induction 1 as [|x l H H' IH]; intro Hl'; simpl.
+   - constructor.
+   - destruct (set_mem x l'); auto.
+     constructor; auto. rewrite set_inter_iff; tauto.
+  Qed.
+
   Lemma set_diff_intro :
    forall (a:A) (x y:set),
      set_In a x -> ~ set_In a y -> set_In a (set_diff x y).
@@ -360,6 +449,20 @@ Section first_definitions.
   rewrite H; trivial.
   Qed.
 
+  Lemma set_diff_iff a l l' : In a (set_diff l l') <-> In a l /\ ~In a l'.
+  Proof.
+  split.
+  - split; [eapply set_diff_elim1 | eapply set_diff_elim2]; eauto.
+  - destruct 1. now apply set_diff_intro.
+  Qed.
+
+  Lemma set_diff_nodup l l' : NoDup l -> NoDup l' -> NoDup (set_diff l l').
+  Proof.
+   induction 1 as [|x l H H' IH]; intro Hl'; simpl.
+   - constructor.
+   - destruct (set_mem x l'); auto using set_add_nodup.
+  Qed.
+
   Lemma set_diff_trivial : forall (a:A) (x:set), ~ set_In a (set_diff x x).
   red; intros a x H.
   apply (set_diff_elim2 _ _ _ H).
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index 7ec3d250..1c302b22 100644
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -51,7 +51,7 @@ Lemma tl_nth_tl :
 Proof.
   simple induction n; simpl; auto.
 Qed.
-Hint Resolve tl_nth_tl: datatypes v62.
+Hint Resolve tl_nth_tl: datatypes.
 
 Lemma Str_nth_tl_plus :
  forall (n m:nat) (s:Stream),
diff --git a/theories/Logic/ClassicalFacts.v b/theories/Logic/ClassicalFacts.v
index c947062a..afd64efd 100644
--- a/theories/Logic/ClassicalFacts.v
+++ b/theories/Logic/ClassicalFacts.v
@@ -34,6 +34,8 @@ Table of contents:
 
 3 3. Independence of general premises and drinker's paradox
 
+4. Classical logic and principle of unrestricted minimization
+
 *)
 
 (************************************************************************)
@@ -658,3 +660,79 @@ Proof.
     exists x; intro; exact Hx.
     exists x0; exact Hnot.
 Qed.
+
+(** ** Principle of unrestricted minimization *)
+
+Require Import Coq.Arith.PeanoNat.
+
+Definition Minimal (P:nat -> Prop) (n:nat) : Prop :=
+  P n /\ forall k, P k -> n<=k.
+
+Definition Minimization_Property (P : nat -> Prop) : Prop :=
+  forall n, P n -> exists m, Minimal P m.
+
+Section Unrestricted_minimization_entails_excluded_middle.
+
+  Hypothesis unrestricted_minimization: forall P, Minimization_Property P.
+
+  Theorem unrestricted_minimization_entails_excluded_middle : forall A, A\/~A.
+  Proof.
+    intros A.
+    pose (P := fun n:nat => n=0/\A \/ n=1).
+    assert (P 1) as h.
+    { unfold P. intuition. }
+    assert (P 0 <-> A) as p₀.
+    { split.
+      + intros [[_ h₀]|[=]]. assumption.
+      + unfold P. tauto. }
+    apply unrestricted_minimization in h as ([|[|m]] & hm & hmm).
+    + intuition.
+    + right.
+      intros HA. apply p₀, hmm, PeanoNat.Nat.nle_succ_0 in HA. assumption.
+    + destruct hm as [([=],_) | [=] ].
+  Qed.
+
+End Unrestricted_minimization_entails_excluded_middle.
+
+Require Import Wf_nat.
+
+Section Excluded_middle_entails_unrestricted_minimization.
+
+  Hypothesis em : forall A, A\/~A.
+
+  Theorem excluded_middle_entails_unrestricted_minimization : 
+    forall P, Minimization_Property P.
+  Proof.
+    intros P n HPn.
+    assert (dec : forall n, P n \/ ~ P n) by auto using em.
+    assert (ex : exists n, P n) by (exists n; assumption).
+    destruct (dec_inh_nat_subset_has_unique_least_element P dec ex) as (n' & HPn' & _).
+    exists n'. assumption.
+  Qed.
+
+End Excluded_middle_entails_unrestricted_minimization.
+
+(** However, minimization for a given predicate does not necessarily imply
+    decidability of this predicate *)
+
+Section Example_of_undecidable_predicate_with_the_minimization_property.
+
+  Variable s : nat -> bool.
+
+  Let P n := exists k, n<=k /\ s k = true.
+
+  Example undecidable_predicate_with_the_minimization_property : 
+    Minimization_Property P.
+  Proof.
+    unfold Minimization_Property.
+    intros h hn.
+    exists 0. split.
+    + unfold P in *. destruct hn as (k&hk₁&hk₂).
+      exists k. split.
+      * rewrite <- hk₁.
+        apply PeanoNat.Nat.le_0_l.
+      * assumption.
+    + intros **. apply PeanoNat.Nat.le_0_l.
+  Qed.
+
+End Example_of_undecidable_predicate_with_the_minimization_property.
diff --git a/theories/Logic/Decidable.v b/theories/Logic/Decidable.v
index 2ba7253c..8b6054f9 100644
--- a/theories/Logic/Decidable.v
+++ b/theories/Logic/Decidable.v
@@ -50,7 +50,7 @@ Qed.
 Theorem dec_iff :
  forall A B:Prop, decidable A -> decidable B -> decidable (A<->B).
 Proof.
-unfold decidable; tauto.
+unfold decidable. tauto.
 Qed.
 
 Theorem not_not : forall P:Prop, decidable P -> ~ ~ P -> P.
diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index f3a2783e..5ef86b8e 100644
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.v
@@ -33,5 +33,5 @@ Export EqdepTheory.
 
 (** Exported hints *)
 
-Hint Resolve eq_dep_eq: eqdep v62.
+Hint Resolve eq_dep_eq: eqdep.
 Hint Resolve inj_pair2 inj_pairT2: eqdep.
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v
index 30e26c7c..bd59159b 100644
--- a/theories/Logic/EqdepFacts.v
+++ b/theories/Logic/EqdepFacts.v
@@ -164,7 +164,7 @@ Proof.
   split; auto using eq_sig_eq_dep, eq_dep_eq_sig.
 Qed.
 
-(** Dependent equality is equivalent tco a dependent pair of equalities *)
+(** Dependent equality is equivalent to a dependent pair of equalities *)
 
 Set Implicit Arguments.
 
diff --git a/theories/Logic/Hurkens.v b/theories/Logic/Hurkens.v
index 8ded7476..841f843c 100644
--- a/theories/Logic/Hurkens.v
+++ b/theories/Logic/Hurkens.v
@@ -631,6 +631,8 @@ End NoRetractFromTypeToProp.
 
 Module TypeNeqSmallType.
 
+Unset Universe Polymorphism.
+
 Section Paradox.
 
 (** ** Universe [U] is equal to one of its elements. *)
@@ -655,7 +657,6 @@ Proof.
   reflexivity.
 Qed.
 
-
 Theorem paradox : False.
 Proof.
   Generic.paradox p.
diff --git a/theories/Logic/PropFacts.v b/theories/Logic/PropFacts.v
new file mode 100644
index 00000000..309539e5
--- /dev/null
+++ b/theories/Logic/PropFacts.v
@@ -0,0 +1,50 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * Basic facts about Prop as a type *)
+
+(** An intuitionistic theorem from topos theory [[LambekScott]]
+
+References:
+
+[[LambekScott]] Jim Lambek, Phil J. Scott, Introduction to higher
+order categorical logic, Cambridge Studies in Advanced Mathematics
+(Book 7), 1988.
+
+*)
+
+Theorem injection_is_involution_in_Prop
+  (f : Prop -> Prop)
+  (inj : forall A B, (f A <-> f B) -> (A <-> B))
+  (ext : forall A B, A <-> B -> f A <-> f B)
+  : forall A, f (f A) <-> A.
+Proof.
+intros.
+enough (f (f (f A)) <-> f A) by (apply inj; assumption).
+split; intro H.
+- now_show (f A).
+  enough (f A <-> True) by firstorder.
+  enough (f (f A) <-> f True) by (apply inj; assumption).
+  split; intro H'.
+  + now_show (f True).
+    enough (f (f (f A)) <-> f True) by firstorder.
+    apply ext; firstorder.
+  + now_show (f (f A)).
+    enough (f (f A) <-> True) by firstorder.
+    apply inj; firstorder.
+- now_show (f (f (f A))).
+  enough (f A <-> f (f (f A))) by firstorder.
+  apply ext.
+  split; intro H'.
+  + now_show (f (f A)).
+    enough (f A <-> f (f A)) by firstorder.
+    apply ext; firstorder.
+  + now_show A.
+    enough (f A <-> A) by firstorder.
+    apply inj; firstorder.
+Defined.
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index cc023cc3..a3c265a2 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -417,6 +417,7 @@ Local Open Scope Int_scope.
     Let's do its job by hand: *)
 
 Ltac join_tac :=
+ let l := fresh "l" in
  intro l; induction l as [| lh ll _ lx lr Hlr];
    [ | intros x r; induction r as [| rh rl Hrl rx rr _]; unfold join;
      [ | destruct ((rh+2) <? lh) eqn:LT;
diff --git a/theories/MSets/MSetDecide.v b/theories/MSets/MSetDecide.v
index f2555791..9c622fd7 100644
--- a/theories/MSets/MSetDecide.v
+++ b/theories/MSets/MSetDecide.v
@@ -357,17 +357,8 @@ the above form:
         | _ => idtac
       end.
 
-    (** [if t then t1 else t2] executes [t] and, if it does not
-        fail, then [t1] will be applied to all subgoals
-        produced.  If [t] fails, then [t2] is executed. *)
-    Tactic Notation
-      "if" tactic(t)
-      "then" tactic(t1)
-      "else" tactic(t2) :=
-      first [ t; first [ t1 | fail 2 ] | t2 ].
-
     Ltac abstract_term t :=
-      if (is_var t) then fail "no need to abstract a variable"
+      tryif (is_var t) then fail "no need to abstract a variable"
       else (let x := fresh "x" in set (x := t) in *; try clearbody x).
 
     Ltac abstract_elements :=
@@ -478,11 +469,11 @@ the above form:
       repeat (
         match goal with
         | H : context [ @Logic.eq ?T ?x ?y ] |- _ =>
-          if (change T with E.t in H) then fail
-          else if (change T with t in H) then fail
+          tryif (change T with E.t in H) then fail
+          else tryif (change T with t in H) then fail
           else clear H
         | H : ?P |- _ =>
-          if prop (MSet_Prop P) holds by
+          tryif prop (MSet_Prop P) holds by
             (auto 100 with MSet_Prop)
           then fail
           else clear H
@@ -747,7 +738,7 @@ the above form:
     | H: (In ?x ?r) -> False |- (E.eq ?y ?x) -> False =>
       contradict H; fsetdec_body
     | H: ?P -> False |- ?Q -> False =>
-      if prop (MSet_elt_Prop P) holds by
+      tryif prop (MSet_elt_Prop P) holds by
         (auto 100 with MSet_Prop)
       then (contradict H; fsetdec_body)
       else fsetdec_body
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index bd881168..74a7f6df 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -345,6 +345,9 @@ Module Type WRawSets (E : DecidableType).
       predicate [Ok]. If [Ok] isn't decidable, [isok] may be the
       always-false function. *)
   Parameter isok : t -> bool.
+  (** MS: 
+    Dangerous instance, the [isok s = true] hypothesis cannot be discharged
+   with typeclass resolution. Is it really an instance? *)
   Declare Instance isok_Ok s `(isok s = true) : Ok s | 10.
 
   (** Logical predicates *)
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index fb0d1ad9..05c20eb8 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -8,7 +8,7 @@
 
 (** * Finite sets library *)
 
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
     interface [MSetInterface.S] using strictly ordered list. *)
 
 Require Export MSetInterface OrdersFacts OrdersLists.
diff --git a/theories/MSets/MSetPositive.v b/theories/MSets/MSetPositive.v
index 8dd240f4..be95a037 100644
--- a/theories/MSets/MSetPositive.v
+++ b/theories/MSets/MSetPositive.v
@@ -908,10 +908,10 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
       destruct o.
         intros x H. injection H; intros; subst. reflexivity.
         revert IHl. case choose.
-          intros p Hp x H. injection H; intros; subst; clear H. apply Hp.
+          intros p Hp x H. injection H as <-. apply Hp.
            reflexivity.
           intros _ x. revert IHr. case choose.
-            intros p Hp H. injection H; intros; subst; clear H. apply Hp.
+            intros p Hp H. injection H as <-. apply Hp.
             reflexivity.
             intros. discriminate.
   Qed.
@@ -968,11 +968,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
    induction s as [| l IHl o r IHr]; simpl.
      intros. discriminate.
      intros x. destruct (min_elt l); intros.
-       injection H. intros <-. apply IHl. reflexivity.
+       injection H as <-. apply IHl. reflexivity.
        destruct o; simpl.
-         injection H. intros <-. reflexivity.
+         injection H as <-. reflexivity.
          destruct (min_elt r); simpl in *.
-           injection H. intros <-. apply IHr. reflexivity.
+           injection H as <-. apply IHr. reflexivity.
            discriminate.
   Qed.
 
@@ -996,15 +996,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     induction s as [|l IHl o r IHr]; intros x y H H'.
       discriminate.
       simpl in H. case_eq (min_elt l).
-        intros p Hp. rewrite Hp in H. injection H; intros <-.
+        intros p Hp. rewrite Hp in H. injection H as <-.
         destruct y as [z|z|]; simpl; intro; trivial. apply (IHl p z); trivial.
         intro Hp; rewrite Hp in H. apply min_elt_spec3 in Hp.
         destruct o.
-          injection H. intros <- Hl. clear H.
+          injection H as <-. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (min_elt r).
-            injection H. intros <-. clear H.
+            injection H as <-.
             destruct y as [z|z|].
               apply (IHr e z); trivial.
               elim (Hp _ H').
@@ -1021,11 +1021,11 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
    induction s as [| l IHl o r IHr]; simpl.
      intros. discriminate.
      intros x. destruct (max_elt r); intros.
-       injection H. intros <-. apply IHr. reflexivity.
+       injection H as <-. apply IHr. reflexivity.
        destruct o; simpl.
-         injection H. intros <-. reflexivity.
+         injection H as <-. reflexivity.
          destruct (max_elt l); simpl in *.
-           injection H. intros <-. apply IHl. reflexivity.
+           injection H as <-. apply IHl. reflexivity.
            discriminate.
   Qed.
 
@@ -1049,15 +1049,15 @@ Module PositiveSet <: S with Module E:=PositiveOrderedTypeBits.
     induction s as [|l IHl o r IHr]; intros x y H H'.
       discriminate.
       simpl in H. case_eq (max_elt r).
-        intros p Hp. rewrite Hp in H. injection H; intros <-.
+        intros p Hp. rewrite Hp in H. injection H as <-.
         destruct y as [z|z|]; simpl; intro; trivial. apply (IHr p z); trivial.
         intro Hp; rewrite Hp in H. apply max_elt_spec3 in Hp.
         destruct o.
-          injection H. intros <- Hl. clear H.
+          injection H as <-. intros Hl.
           destruct y as [z|z|]; simpl; trivial. elim (Hp _ H').
 
           destruct (max_elt l).
-            injection H. intros <-. clear H.
+            injection H as <-.
             destruct y as [z|z|].
               elim (Hp _ H').
               apply (IHl e z); trivial.
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index 751d4f35..83a2343d 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -911,7 +911,7 @@ Proof.
      { inversion_clear O.
        assert (InT x l) by now apply min_elt_spec1. auto. }
      simpl. case X.compare_spec; try order.
-     destruct lc; injection E; clear E; intros; subst l s0; auto.
+     destruct lc; injection E; subst l s0; auto.
 Qed.
 
 Lemma remove_min_spec1 s x s' `{Ok s}:
@@ -1948,7 +1948,7 @@ Module Make (X: Orders.OrderedType) <:
  generalize (fun x s' => @Raw.remove_min_spec1 s x s' Hs).
  set (P := Raw.remove_min_ok s). clearbody P.
  destruct (Raw.remove_min s) as [(x0,s0)|]; try easy.
- intros H U. injection U. clear U; intros; subst. simpl.
+ intros H U. injection U as -> <-. simpl.
  destruct (H x s0); auto. subst; intuition.
  Qed.
 
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 372acd56..2ac57a93 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -8,7 +8,7 @@
 
 (** * Finite sets library *)
 
-(** This file proposes an implementation of the non-dependant
+(** This file proposes an implementation of the non-dependent
     interface [MSetWeakInterface.S] using lists without redundancy. *)
 
 Require Import MSetInterface.
diff --git a/theories/Numbers/BigNumPrelude.v b/theories/Numbers/BigNumPrelude.v
index 45a7527c..bd893087 100644
--- a/theories/Numbers/BigNumPrelude.v
+++ b/theories/Numbers/BigNumPrelude.v
@@ -10,7 +10,7 @@
 
 (** * BigNumPrelude *)
 
-(** Auxillary functions & theorems used for arbitrary precision efficient
+(** Auxiliary functions & theorems used for arbitrary precision efficient
     numbers. *)
 
 
@@ -22,7 +22,7 @@ Require Export Zpow_facts.
 Declare ML Module "numbers_syntax_plugin".
 
 (* *** Nota Bene ***
-   All results that were general enough has been moved in ZArith.
+   All results that were general enough have been moved in ZArith.
    Only remain here specialized lemmas and compatibility elements.
    (P.L. 5/11/2007).
 *)
diff --git a/theories/Numbers/Cyclic/Int31/Ring31.v b/theories/Numbers/Cyclic/Int31/Ring31.v
index 215b8bd5..d160f5f1 100644
--- a/theories/Numbers/Cyclic/Int31/Ring31.v
+++ b/theories/Numbers/Cyclic/Int31/Ring31.v
@@ -19,13 +19,13 @@ Local Open Scope list_scope.
 
 Ltac isInt31cst_lst l :=
  match l with
- | nil => constr:true
+ | nil => constr:(true)
  | ?t::?l => match t with
                | D1 => isInt31cst_lst l
                | D0 => isInt31cst_lst l
-               | _ => constr:false
+               | _ => constr:(false)
              end
- | _ => constr:false
+ | _ => constr:(false)
  end.
 
 Ltac isInt31cst t :=
@@ -38,17 +38,17 @@ Ltac isInt31cst t :=
       ::i11::i12::i13::i14::i15::i16::i17::i18::i19::i20
       ::i21::i22::i23::i24::i25::i26::i27::i28::i29::i30::nil)
     in isInt31cst_lst l
- | Int31.On => constr:true
- | Int31.In => constr:true
- | Int31.Tn => constr:true
- | Int31.Twon => constr:true
- | _ => constr:false
+ | Int31.On => constr:(true)
+ | Int31.In => constr:(true)
+ | Int31.Tn => constr:(true)
+ | Int31.Twon => constr:(true)
+ | _ => constr:(false)
  end.
 
 Ltac Int31cst t :=
  match isInt31cst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 (** The generic ring structure inferred from the Cyclic structure *)
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index c115a831..04fc5a8d 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -369,7 +369,7 @@ Section ZModulo.
  assert (Z.div_eucl ([|x|]*[|y|]) wB = (([|x|]*[|y|])/wB,([|x|]*[|y|]) mod wB)).
   unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
  generalize (Z_div_mod ([|x|]*[|y|]) wB wB_pos); destruct Z.div_eucl as (h,l).
- destruct 1; injection H; clear H; intros.
+ destruct 1; injection H as ? ?.
  rewrite H0.
  assert ([|l|] = l).
   apply Zmod_small; auto.
@@ -411,7 +411,7 @@ Section ZModulo.
   unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
  generalize (Z_div_mod [|a|] [|b|] H0).
  destruct Z.div_eucl as (q,r); destruct 1; intros.
- injection H1; clear H1; intros.
+ injection H1 as ? ?.
  assert ([|r|]=r).
   apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
    auto with zarith.
@@ -522,7 +522,7 @@ Section ZModulo.
   unfold Z.modulo, Z.div; destruct Z.div_eucl; auto.
  generalize (Z_div_mod a [|b|] H3).
  destruct Z.div_eucl as (q,r); destruct 1; intros.
- injection H4; clear H4; intros.
+ injection H4 as ? ?.
  assert ([|r|]=r).
   apply Zmod_small; generalize (Z_mod_lt b wB wB_pos); fold [|b|];
    auto with zarith.
diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v
index 278e1bcf..c2fa69e5 100644
--- a/theories/Numbers/Integer/Abstract/ZDivEucl.v
+++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v
@@ -30,18 +30,23 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv.
     We just ignore them here.
 *)
 
-Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod' A).
- Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= a mod b < abs b.
+Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod A).
+ Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= B.modulo a b < abs b.
 End EuclidSpec.
 
 Module Type ZEuclid (Z:ZAxiomsSig) := NZDiv.NZDiv Z <+ EuclidSpec Z.
-Module Type ZEuclid' (Z:ZAxiomsSig) := NZDiv.NZDiv' Z <+ EuclidSpec Z.
 
 Module ZEuclidProp
  (Import A : ZAxiomsSig')
  (Import B : ZMulOrderProp A)
  (Import C : ZSgnAbsProp A B)
- (Import D : ZEuclid' A).
+ (Import D : ZEuclid A).
+
+ (** We put notations in a scope, to avoid warnings about
+     redefinitions of notations *)
+ Infix "/" := D.div : euclid.
+ Infix "mod" := D.modulo : euclid.
+ Local Open Scope euclid.
 
  Module Import Private_NZDiv := Nop <+ NZDivProp A D B.
 
@@ -615,4 +620,3 @@ intros (c,Hc). rewrite Hc. now apply mod_mul.
 Qed.
 
 End ZEuclidProp.
-
diff --git a/theories/Numbers/Integer/BigZ/BigZ.v b/theories/Numbers/Integer/BigZ/BigZ.v
index ec495d09..7c76011f 100644
--- a/theories/Numbers/Integer/BigZ/BigZ.v
+++ b/theories/Numbers/Integer/BigZ/BigZ.v
@@ -138,7 +138,7 @@ intros NEQ.
 generalize (BigZ.spec_div_eucl a b).
 generalize (Z_div_mod_full [a] [b] NEQ).
 destruct BigZ.div_eucl as (q,r), Z.div_eucl as (q',r').
-intros (EQ,_). injection 1. intros EQr EQq.
+intros (EQ,_). injection 1 as EQr EQq.
 BigZ.zify. rewrite EQr, EQq; auto.
 Qed.
 
@@ -148,26 +148,26 @@ Ltac isBigZcst t :=
  match t with
  | BigZ.Pos ?t => isBigNcst t
  | BigZ.Neg ?t => isBigNcst t
- | BigZ.zero => constr:true
- | BigZ.one => constr:true
- | BigZ.two => constr:true
- | BigZ.minus_one => constr:true
- | _ => constr:false
+ | BigZ.zero => constr:(true)
+ | BigZ.one => constr:(true)
+ | BigZ.two => constr:(true)
+ | BigZ.minus_one => constr:(true)
+ | _ => constr:(false)
  end.
 
 Ltac BigZcst t :=
  match isBigZcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 Ltac BigZ_to_N t :=
  match t with
  | BigZ.Pos ?t => BigN_to_N t
- | BigZ.zero => constr:0%N
- | BigZ.one => constr:1%N
- | BigZ.two => constr:2%N
- | _ => constr:NotConstant
+ | BigZ.zero => constr:(0%N)
+ | BigZ.one => constr:(1%N)
+ | BigZ.two => constr:(2%N)
+ | _ => constr:(NotConstant)
  end.
 
 (** Registration for the "ring" tactic *)
diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v
index 8673b8a5..fec6e068 100644
--- a/theories/Numbers/Integer/BigZ/ZMake.v
+++ b/theories/Numbers/Integer/BigZ/ZMake.v
@@ -147,7 +147,7 @@ Module Make (NN:NType) <: ZType.
  Proof.
  apply Bool.eq_iff_eq_true.
  rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
- destruct Z.compare; split; try easy. now destruct 1.
+ now destruct Z.compare; split.
  Qed.
 
  Definition min n m := match compare n m with Gt => m | _ => n end.
@@ -427,13 +427,13 @@ Module Make (NN:NType) <: ZType.
  (* Pos Neg *)
  generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr;
+ try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr;
       simpl; rewrite Hq, NN.spec_0; auto).
  change (- Zpos py) with (Zneg py).
  assert (GT : Zpos py > 0) by (compute; auto).
  generalize (Z_div_mod (Zpos px) (Zpos py) GT).
  unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r').
- intros (EQ,MOD). injection 1. intros Hr' Hq'.
+ intros (EQ,MOD). injection 1 as Hq' Hr'.
  rewrite NN.spec_eqb, NN.spec_0, Hr'.
  break_nonneg r pr EQr.
  subst; simpl. rewrite NN.spec_0; auto.
@@ -442,13 +442,13 @@ Module Make (NN:NType) <: ZType.
  (* Neg Pos *)
  generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite NN.spec_eqb, NN.spec_0, Hr;
+ try (injection 1 as Hq Hr; rewrite NN.spec_eqb, NN.spec_0, Hr;
       simpl; rewrite Hq, NN.spec_0; auto).
  change (- Zpos px) with (Zneg px).
  assert (GT : Zpos py > 0) by (compute; auto).
  generalize (Z_div_mod (Zpos px) (Zpos py) GT).
  unfold Z.div_eucl. destruct (Z.pos_div_eucl px (Zpos py)) as (q',r').
- intros (EQ,MOD). injection 1. intros Hr' Hq'.
+ intros (EQ,MOD). injection 1 as Hq' Hr'.
  rewrite NN.spec_eqb, NN.spec_0, Hr'.
  break_nonneg r pr EQr.
  subst; simpl. rewrite NN.spec_0; auto.
@@ -457,7 +457,7 @@ Module Make (NN:NType) <: ZType.
  (* Neg Neg *)
  generalize (NN.spec_div_eucl x y); destruct (NN.div_eucl x y) as (q,r).
  break_nonneg x px EQx; break_nonneg y py EQy;
- try (injection 1; intros Hr Hq; rewrite Hr, Hq; auto).
+ try (injection 1 as -> ->; auto).
  simpl. intros <-; auto.
  Qed.
 
diff --git a/theories/Numbers/NatInt/NZGcd.v b/theories/Numbers/NatInt/NZGcd.v
index 1d367294..44088f8c 100644
--- a/theories/Numbers/NatInt/NZGcd.v
+++ b/theories/Numbers/NatInt/NZGcd.v
@@ -60,8 +60,6 @@ Proof.
  intros n. exists 0. now nzsimpl.
 Qed.
 
-Hint Rewrite divide_1_l divide_0_r : nz.
-
 Lemma divide_0_l : forall n, (0 | n) -> n==0.
 Proof.
  intros n (m,Hm). revert Hm. now nzsimpl.
diff --git a/theories/Numbers/Natural/BigN/BigN.v b/theories/Numbers/Natural/BigN/BigN.v
index 29a1145e..e8ff516f 100644
--- a/theories/Numbers/Natural/BigN/BigN.v
+++ b/theories/Numbers/Natural/BigN/BigN.v
@@ -110,7 +110,7 @@ intros NEQ.
 generalize (BigN.spec_div_eucl a b).
 generalize (Z_div_mod_full [a] [b] NEQ).
 destruct BigN.div_eucl as (q,r), Z.div_eucl as (q',r').
-intros (EQ,_). injection 1. intros EQr EQq.
+intros (EQ,_). injection 1 as EQr EQq.
 BigN.zify. rewrite EQr, EQq; auto.
 Qed.
 
@@ -119,10 +119,10 @@ Qed.
 
 Ltac isStaticWordCst t :=
  match t with
- | W0 => constr:true
+ | W0 => constr:(true)
  | WW ?t1 ?t2 =>
    match isStaticWordCst t1 with
-   | false => constr:false
+   | false => constr:(false)
    | true => isStaticWordCst t2
    end
  | _ => isInt31cst t
@@ -139,30 +139,30 @@ Ltac isBigNcst t :=
  | BigN.N6 ?t => isStaticWordCst t
  | BigN.Nn ?n ?t => match isnatcst n with
    | true => isStaticWordCst t
-   | false => constr:false
+   | false => constr:(false)
    end
- | BigN.zero => constr:true
- | BigN.one => constr:true
- | BigN.two => constr:true
- | _ => constr:false
+ | BigN.zero => constr:(true)
+ | BigN.one => constr:(true)
+ | BigN.two => constr:(true)
+ | _ => constr:(false)
  end.
 
 Ltac BigNcst t :=
  match isBigNcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 Ltac BigN_to_N t :=
  match isBigNcst t with
  | true => eval vm_compute in (BigN.to_N t)
- | false => constr:NotConstant
+ | false => constr:(NotConstant)
  end.
 
 Ltac Ncst t :=
  match isNcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 (** Registration for the "ring" tactic *)
diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v
index 98949736..1425041a 100644
--- a/theories/Numbers/Natural/BigN/NMake.v
+++ b/theories/Numbers/Natural/BigN/NMake.v
@@ -338,7 +338,7 @@ Module Make (W0:CyclicType) <: NType.
  Proof.
  apply eq_iff_eq_true.
  rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare.
- destruct Z.compare; split; try easy. now destruct 1.
+ now destruct Z.compare; split.
  Qed.
 
  Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end.
diff --git a/theories/Numbers/Natural/BigN/NMake_gen.ml b/theories/Numbers/Natural/BigN/NMake_gen.ml
index 601fa108..5177fae6 100644
--- a/theories/Numbers/Natural/BigN/NMake_gen.ml
+++ b/theories/Numbers/Natural/BigN/NMake_gen.ml
@@ -147,7 +147,7 @@ pr
   pr " Local Notation Size := (SizePlus O).";
   pr "";
 
-  pr " Tactic Notation \"do_size\" tactic(t) := do %i t." (size+1);
+  pr " Tactic Notation (at level 3) \"do_size\" tactic3(t) := do %i t." (size+1);
   pr "";
 
   pr " Definition dom_t n := match n with";
diff --git a/theories/Numbers/Natural/Peano/NPeano.v b/theories/Numbers/Natural/Peano/NPeano.v
index 58b1b018..d0168bd9 100644
--- a/theories/Numbers/Natural/Peano/NPeano.v
+++ b/theories/Numbers/Natural/Peano/NPeano.v
@@ -8,8 +8,88 @@
 (*                      Evgeny Makarov, INRIA, 2007                     *)
 (************************************************************************)
 
-Require Import PeanoNat NAxioms.
+Require Import PeanoNat Even NAxioms.
 
-(** * [PeanoNat.Nat] already implements [NAxiomSig] *)
+(** This file is DEPRECATED ! Use [PeanoNat] (or [Arith]) instead. *)
+
+(** [PeanoNat.Nat] already implements [NAxiomSig] *)
 
 Module Nat <: NAxiomsSig := Nat.
+
+(** Compat notations for stuff that used to be at the beginning of NPeano. *)
+
+Notation leb := Nat.leb (compat "8.4").
+Notation ltb := Nat.ltb (compat "8.4").
+Notation leb_le := Nat.leb_le (compat "8.4").
+Notation ltb_lt := Nat.ltb_lt (compat "8.4").
+Notation pow := Nat.pow (compat "8.4").
+Notation pow_0_r := Nat.pow_0_r (compat "8.4").
+Notation pow_succ_r := Nat.pow_succ_r (compat "8.4").
+Notation square := Nat.square (compat "8.4").
+Notation square_spec := Nat.square_spec (compat "8.4").
+Notation Even := Nat.Even (compat "8.4").
+Notation Odd := Nat.Odd (compat "8.4").
+Notation even := Nat.even (compat "8.4").
+Notation odd := Nat.odd (compat "8.4").
+Notation even_spec := Nat.even_spec (compat "8.4").
+Notation odd_spec := Nat.odd_spec (compat "8.4").
+
+Lemma Even_equiv n : Even n <-> Even.even n.
+Proof. symmetry. apply Even.even_equiv. Qed.
+Lemma Odd_equiv n : Odd n <-> Even.odd n.
+Proof. symmetry. apply Even.odd_equiv. Qed.
+
+Notation divmod := Nat.divmod (compat "8.4").
+Notation div := Nat.div (compat "8.4").
+Notation modulo := Nat.modulo (compat "8.4").
+Notation divmod_spec := Nat.divmod_spec (compat "8.4").
+Notation div_mod := Nat.div_mod (compat "8.4").
+Notation mod_bound_pos := Nat.mod_bound_pos (compat "8.4").
+Notation sqrt_iter := Nat.sqrt_iter (compat "8.4").
+Notation sqrt := Nat.sqrt (compat "8.4").
+Notation sqrt_iter_spec := Nat.sqrt_iter_spec (compat "8.4").
+Notation sqrt_spec := Nat.sqrt_spec (compat "8.4").
+Notation log2_iter := Nat.log2_iter (compat "8.4").
+Notation log2 := Nat.log2 (compat "8.4").
+Notation log2_iter_spec := Nat.log2_iter_spec (compat "8.4").
+Notation log2_spec := Nat.log2_spec (compat "8.4").
+Notation log2_nonpos := Nat.log2_nonpos (compat "8.4").
+Notation gcd := Nat.gcd (compat "8.4").
+Notation divide := Nat.divide (compat "8.4").
+Notation gcd_divide := Nat.gcd_divide (compat "8.4").
+Notation gcd_divide_l := Nat.gcd_divide_l (compat "8.4").
+Notation gcd_divide_r := Nat.gcd_divide_r (compat "8.4").
+Notation gcd_greatest := Nat.gcd_greatest (compat "8.4").
+Notation testbit := Nat.testbit (compat "8.4").
+Notation shiftl := Nat.shiftl (compat "8.4").
+Notation shiftr := Nat.shiftr (compat "8.4").
+Notation bitwise := Nat.bitwise (compat "8.4").
+Notation land := Nat.land (compat "8.4").
+Notation lor := Nat.lor (compat "8.4").
+Notation ldiff := Nat.ldiff (compat "8.4").
+Notation lxor := Nat.lxor (compat "8.4").
+Notation double_twice := Nat.double_twice (compat "8.4").
+Notation testbit_0_l := Nat.testbit_0_l (compat "8.4").
+Notation testbit_odd_0 := Nat.testbit_odd_0 (compat "8.4").
+Notation testbit_even_0 := Nat.testbit_even_0 (compat "8.4").
+Notation testbit_odd_succ := Nat.testbit_odd_succ (compat "8.4").
+Notation testbit_even_succ := Nat.testbit_even_succ (compat "8.4").
+Notation shiftr_spec := Nat.shiftr_spec (compat "8.4").
+Notation shiftl_spec_high := Nat.shiftl_spec_high (compat "8.4").
+Notation shiftl_spec_low := Nat.shiftl_spec_low (compat "8.4").
+Notation div2_bitwise := Nat.div2_bitwise (compat "8.4").
+Notation odd_bitwise := Nat.odd_bitwise (compat "8.4").
+Notation div2_decr := Nat.div2_decr (compat "8.4").
+Notation testbit_bitwise_1 := Nat.testbit_bitwise_1 (compat "8.4").
+Notation testbit_bitwise_2 := Nat.testbit_bitwise_2 (compat "8.4").
+Notation land_spec := Nat.land_spec (compat "8.4").
+Notation ldiff_spec := Nat.ldiff_spec (compat "8.4").
+Notation lor_spec := Nat.lor_spec (compat "8.4").
+Notation lxor_spec := Nat.lxor_spec (compat "8.4").
+
+Infix "<=?" := Nat.leb (at level 70) : nat_scope.
+Infix "<?" := Nat.ltb (at level 70) : nat_scope.
+Infix "^" := Nat.pow : nat_scope.
+Infix "/" := Nat.div : nat_scope.
+Infix "mod" := Nat.modulo (at level 40, no associativity) : nat_scope.
+Notation "( x | y )" := (Nat.divide x y) (at level 0) : nat_scope.
diff --git a/theories/Numbers/Rational/BigQ/BigQ.v b/theories/Numbers/Rational/BigQ/BigQ.v
index fe38ea4f..850afe53 100644
--- a/theories/Numbers/Rational/BigQ/BigQ.v
+++ b/theories/Numbers/Rational/BigQ/BigQ.v
@@ -104,18 +104,18 @@ Ltac isBigQcst t :=
  | BigQ.Qz ?t => isBigZcst t
  | BigQ.Qq ?n ?d => match isBigZcst n with
              | true => isBigNcst d
-             | false => constr:false
+             | false => constr:(false)
              end
- | BigQ.zero => constr:true
- | BigQ.one => constr:true
- | BigQ.minus_one => constr:true
- | _ => constr:false
+ | BigQ.zero => constr:(true)
+ | BigQ.one => constr:(true)
+ | BigQ.minus_one => constr:(true)
+ | _ => constr:(false)
  end.
 
 Ltac BigQcst t :=
  match isBigQcst t with
- | true => constr:t
- | false => constr:NotConstant
+ | true => constr:(t)
+ | false => constr:(NotConstant)
  end.
 
 Add Field BigQfield : BigQfieldth
diff --git a/theories/Numbers/Rational/BigQ/QMake.v b/theories/Numbers/Rational/BigQ/QMake.v
index 4ac36425..b9fed9d5 100644
--- a/theories/Numbers/Rational/BigQ/QMake.v
+++ b/theories/Numbers/Rational/BigQ/QMake.v
@@ -1050,13 +1050,13 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  Theorem spec_of_Qc: forall q, [[of_Qc q]] = q.
  Proof.
  intros; apply Qc_decomp; simpl; intros.
- rewrite strong_spec_of_Qc; auto.
+ rewrite strong_spec_of_Qc. apply canon.
  Qed.
 
  Theorem spec_oppc: forall q, [[opp q]] = -[[q]].
  Proof.
  intros q; unfold Qcopp, to_Qc, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete.
  rewrite spec_opp, <- Qred_opp, Qred_correct.
  apply Qeq_refl.
@@ -1085,10 +1085,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  unfold to_Qc.
  transitivity (Q2Qc ([x] + [y])).
  unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete; apply spec_add; auto.
  unfold Qcplus, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete.
  apply Qplus_comp; apply Qeq_sym; apply Qred_correct.
  Qed.
@@ -1099,10 +1099,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  unfold to_Qc.
  transitivity (Q2Qc ([x] + [y])).
  unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete; apply spec_add_norm; auto.
  unfold Qcplus, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete.
  apply Qplus_comp; apply Qeq_sym; apply Qred_correct.
  Qed.
@@ -1147,10 +1147,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  unfold to_Qc.
  transitivity (Q2Qc ([x] * [y])).
  unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete; apply spec_mul; auto.
  unfold Qcmult, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete.
  apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
  Qed.
@@ -1161,10 +1161,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  unfold to_Qc.
  transitivity (Q2Qc ([x] * [y])).
  unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete; apply spec_mul_norm; auto.
  unfold Qcmult, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete.
  apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
  Qed.
@@ -1185,10 +1185,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  unfold to_Qc.
  transitivity (Q2Qc (/[x])).
  unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete; apply spec_inv; auto.
  unfold Qcinv, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete.
  apply Qinv_comp; apply Qeq_sym; apply Qred_correct.
  Qed.
@@ -1199,10 +1199,10 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  unfold to_Qc.
  transitivity (Q2Qc (/[x])).
  unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete; apply spec_inv_norm; auto.
  unfold Qcinv, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete.
  apply Qinv_comp; apply Qeq_sym; apply Qred_correct.
  Qed.
@@ -1247,13 +1247,13 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  unfold to_Qc.
  transitivity (Q2Qc ([x]^2)).
  unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete; apply spec_square; auto.
  simpl Qcpower.
  replace (Q2Qc [x] * 1) with (Q2Qc [x]); try ring.
  simpl.
  unfold Qcmult, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete.
  apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
  Qed.
@@ -1264,14 +1264,14 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  unfold to_Qc.
  transitivity (Q2Qc ([x]^Zpos p)).
  unfold Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete; apply spec_power_pos; auto.
  induction p using Pos.peano_ind.
  simpl; ring.
  rewrite Pos2Nat.inj_succ; simpl Qcpower.
  rewrite <- IHp; clear IHp.
  unfold Qcmult, Q2Qc.
- apply Qc_decomp; intros _ _; unfold this.
+ apply Qc_decomp; unfold this.
  apply Qred_complete.
  setoid_replace ([x] ^ ' Pos.succ p)%Q with ([x] * [x] ^ ' p)%Q.
  apply Qmult_comp; apply Qeq_sym; apply Qred_correct.
@@ -1281,4 +1281,3 @@ Module Make (NN:NType)(ZZ:ZType)(Import NZ:NType_ZType NN ZZ) <: QType.
  Qed.
 
 End Make.
-
diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v
index a40d9405..8e20fd06 100644
--- a/theories/Numbers/Rational/SpecViaQ/QSig.v
+++ b/theories/Numbers/Rational/SpecViaQ/QSig.v
@@ -115,7 +115,10 @@ Ltac solve_wd2 := intros x x' Hx y y' Hy; qify; now rewrite Hx, Hy.
 Local Obligation Tactic := solve_wd2 || solve_wd1.
 
 Instance : Measure to_Q.
-Instance eq_equiv : Equivalence eq := {}.
+Instance eq_equiv : Equivalence eq.
+Proof.
+  change eq with (RelCompFun Qeq to_Q); apply _.
+Defined.
 
 Program Instance lt_wd : Proper (eq==>eq==>iff) lt.
 Program Instance le_wd : Proper (eq==>eq==>iff) le.
@@ -141,7 +144,10 @@ Proof. intros. qify. destruct (Qcompare_spec [x] [y]); auto. Qed.
 (** Let's implement [TotalOrder] *)
 
 Definition lt_compat := lt_wd.
-Instance lt_strorder : StrictOrder lt := {}.
+Instance lt_strorder : StrictOrder lt.
+Proof.
+  change lt with (RelCompFun Qlt to_Q); apply _.
+Qed.
 
 Lemma le_lteq : forall x y, x<=y <-> x<y \/ x==y.
 Proof. intros. qify. apply Qle_lteq. Qed.
diff --git a/theories/PArith/BinPos.v b/theories/PArith/BinPos.v
index 0ccfad7b..7baf102a 100644
--- a/theories/PArith/BinPos.v
+++ b/theories/PArith/BinPos.v
@@ -201,7 +201,6 @@ Proof.
 Qed.
 
 (** ** No neutral elements for addition *)
-
 Lemma add_no_neutral p q : q + p <> p.
 Proof.
   revert q.
@@ -508,7 +507,7 @@ Qed.
 Lemma mul_xO_discr p q : p~0 * q <> q.
 Proof.
   induction q; try discriminate.
-  rewrite mul_xO_r; injection; assumption.
+  rewrite mul_xO_r; injection; auto.
 Qed.
 
 (** ** Simplification properties of multiplication *)
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 27e1ca84..d6f9bb9d 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -8,7 +8,6 @@
 
 (** Tactics related to (dependent) equality and proof irrelevance. *)
 
-Require Export ProofIrrelevance.
 Require Export JMeq.
 
 Require Import Coq.Program.Tactics.
@@ -143,7 +142,7 @@ Ltac pi_eq_proof_hyp p :=
       | [ H : X = Y |- _ ] =>
         match p with
           | H => fail 2
-          | _ => rewrite (proof_irrelevance (X = Y) p H)
+          | _ => rewrite (UIP _ X Y p H)
         end
       | _ => fail " No hypothesis with same type "
     end
@@ -166,7 +165,7 @@ Hint Rewrite <- eq_rect_eq : refl_id.
    [coerce_* t eq_refl = t]. *)
 
 Lemma JMeq_eq_refl {A} (x : A) : JMeq_eq (@JMeq_refl _ x) = eq_refl.
-Proof. apply proof_irrelevance. Qed.
+Proof. apply UIP. Qed.
 
 Lemma UIP_refl_refl A (x : A) :
   Eqdep.EqdepTheory.UIP_refl A x eq_refl = eq_refl.
@@ -238,8 +237,8 @@ Ltac inject_left H :=
 Ltac inject_right H :=
   progress (inversion H ; subst_right_no_fail ; clear_dups) ; clear H.
 
-Ltac autoinjections_left := repeat autoinjection ltac:inject_left.
-Ltac autoinjections_right := repeat autoinjection ltac:inject_right.
+Ltac autoinjections_left := repeat autoinjection ltac:(inject_left).
+Ltac autoinjections_right := repeat autoinjection ltac:(inject_right).
 
 Ltac simpl_depind := subst_no_fail ; autoinjections ; try discriminates ; 
   simpl_JMeq ; simpl_existTs ; simplify_IH_hyps.
@@ -333,7 +332,7 @@ Ltac simplify_one_dep_elim_term c :=
       (let hyp := fresh in intros hyp ;
         move hyp before y ; revert_until hyp ; generalize dependent y ;
           refine (solution_right _ _ _ _)(*  ; intros until 0 *))
-    | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H)
+    | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; simple injection H; clear H)
     | ?t = ?u -> _ => let hyp := fresh in
       intros hyp ; exfalso ; discriminate
     | ?x = ?y -> _ => let hyp := fresh in
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v
index c8f37318..2a3ec926 100644
--- a/theories/Program/Subset.v
+++ b/theories/Program/Subset.v
@@ -9,6 +9,7 @@
 
 Require Import Coq.Program.Utils.
 Require Import Coq.Program.Equality.
+Require Export ProofIrrelevance.
 
 Local Open Scope program_scope.
 
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v
index 66ca3e57..dfd6b0ea 100644
--- a/theories/Program/Tactics.v
+++ b/theories/Program/Tactics.v
@@ -252,7 +252,7 @@ Ltac autoinjection tac :=
 
 Ltac inject H := progress (inversion H ; subst*; clear_dups) ; clear H.
 
-Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:inject).
+Ltac autoinjections := repeat (clear_dups ; autoinjection ltac:(inject)).
 
 (** Destruct an hypothesis by first copying it to avoid dependencies. *)
 
@@ -264,7 +264,7 @@ Ltac bang :=
   match goal with
     | |- ?x =>
       match x with
-        | appcontext [False_rect _ ?p] => elim p
+        | context [False_rect _ ?p] => elim p
       end
   end.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 154200d7..c490ea51 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -89,7 +89,7 @@ Section Measure_well_founded.
   Lemma measure_wf: well_founded MR.
   Proof with auto.
     unfold well_founded.
-    cut (forall a: M, (fun mm: M => forall a0: T, m a0 = mm -> Acc MR a0) a).
+    cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0).
       intros.
       apply (H (m a))...
     apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)).
@@ -211,7 +211,7 @@ Ltac fold_sub f :=
   match goal with
     | [ |- ?T ] =>
       match T with
-        appcontext C [ @Fix_sub _ _ _ _ _ ?arg ] =>
+        context C [ @Fix_sub _ _ _ _ _ ?arg ] =>
         let app := context C [ f arg ] in
           change app
       end
diff --git a/theories/QArith/Qcabs.v b/theories/QArith/Qcabs.v
new file mode 100644
index 00000000..c0ababff
--- /dev/null
+++ b/theories/QArith/Qcabs.v
@@ -0,0 +1,129 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(** * An absolute value for normalized rational numbers. *)
+
+(** Contributed by Cédric Auger *)
+
+Require Import Qabs Qcanon.
+
+Lemma Qred_abs (x : Q) : Qred (Qabs x) = Qabs (Qred x).
+Proof.
+  destruct x as [[|a|a] d]; simpl; auto;
+  destruct (Pos.ggcd a d) as [x [y z]]; simpl; auto.
+Qed.
+
+Lemma Qcabs_canon (x : Q) : Qred x = x -> Qred (Qabs x) = Qabs x.
+Proof. intros H; now rewrite (Qred_abs x), H. Qed.
+
+Definition Qcabs (x:Qc) : Qc := {| canon := Qcabs_canon x (canon x) |}.
+Notation "[ q ]" := (Qcabs q) (q at next level, format "[ q ]") : Qc_scope.
+
+Ltac Qc_unfolds :=
+  unfold Qcabs, Qcminus, Qcopp, Qcplus, Qcmult, Qcle, Q2Qc, this.
+
+Lemma Qcabs_case (x:Qc) (P : Qc -> Type) :
+  (0 <= x -> P x) -> (x <= 0 -> P (- x)) -> P [x].
+Proof.
+  intros A B.
+  apply (Qabs_case x (fun x => forall Hx, P {|this:=x;canon:=Hx|})).
+  intros; case (Qc_decomp x {|canon:=Hx|}); auto.
+  intros; case (Qc_decomp (-x) {|canon:=Hx|}); auto.
+Qed.
+
+Lemma Qcabs_pos x : 0 <= x -> [x] = x.
+Proof.
+  intro Hx; apply Qc_decomp; Qc_unfolds; fold (this x).
+  set (K := canon [x]); simpl in K; case K; clear K.
+  set (a := x) at 1; case (canon x); subst a; apply Qred_complete.
+  now apply Qabs_pos.
+Qed.
+
+Lemma Qcabs_neg x : x <= 0 -> [x] = - x.
+Proof.
+  intro Hx; apply Qc_decomp; Qc_unfolds; fold (this x).
+  set (K := canon [x]); simpl in K; case K; clear K.
+  now apply Qred_complete; apply Qabs_neg.
+Qed.
+
+Lemma Qcabs_nonneg x : 0 <= [x].
+Proof. intros; apply Qabs_nonneg. Qed.
+
+Lemma Qcabs_opp x : [(-x)] = [x].
+Proof.
+  apply Qc_decomp; Qc_unfolds; fold (this x).
+  set (K := canon [x]); simpl in K; case K; clear K.
+  case Qred_abs; apply Qred_complete; apply Qabs_opp.
+Qed.
+
+Lemma Qcabs_triangle x y : [x+y] <= [x] + [y].
+Proof.
+  Qc_unfolds; case Qred_abs; rewrite !Qred_le; apply Qabs_triangle.
+Qed.
+
+Lemma Qcabs_Qcmult x y : [x*y] = [x]*[y].
+Proof.
+  apply Qc_decomp; Qc_unfolds; fold (this x) (this y); case Qred_abs.
+  apply Qred_complete; apply Qabs_Qmult.
+Qed.
+
+Lemma Qcabs_Qcminus x y: [x-y] = [y-x].
+Proof.
+  apply Qc_decomp; Qc_unfolds; fold (this x) (this y) (this (-x)) (this (-y)).
+  set (a := x) at 2; case (canon x); subst a.
+  set (a := y) at 1; case (canon y); subst a.
+  rewrite !Qred_opp; fold (Qred x - Qred y)%Q (Qred y - Qred x)%Q.
+  repeat case Qred_abs; f_equal; apply Qabs_Qminus.
+Qed.
+
+Lemma Qcle_Qcabs x : x <= [x].
+Proof. apply Qle_Qabs. Qed.
+
+Lemma Qcabs_triangle_reverse x y : [x] - [y] <= [x - y].
+Proof.
+  unfold Qcle, Qcabs, Qcminus, Qcplus, Qcopp, Q2Qc, this;
+  fold (this x) (this y) (this (-x)) (this (-y)).
+  case Qred_abs; rewrite !Qred_le, !Qred_opp, Qred_abs.
+  apply Qabs_triangle_reverse.
+Qed.
+
+Lemma Qcabs_Qcle_condition x y : [x] <= y <-> -y <= x <= y.
+Proof.
+  Qc_unfolds; fold (this x) (this y).
+  destruct (Qabs_Qle_condition x y) as [A B].
+  split; intros H.
+  + destruct (A H) as [X Y]; split; auto.
+    now case (canon x); apply Qred_le.
+  + destruct H as [X Y]; apply B; split; auto.
+    now case (canon y); case Qred_opp.
+Qed.
+
+Lemma Qcabs_diff_Qcle_condition x y r : [x-y] <= r <-> x - r <= y <= x + r.
+Proof.
+  Qc_unfolds; fold (this x) (this y) (this r).
+  case Qred_abs; repeat rewrite Qred_opp.
+  set (a := y) at 1; case (canon y); subst a.
+  set (a := r) at 2; case (canon r); subst a.
+  set (a := Qred r) at 2 3;
+  assert (K := canon (Q2Qc r)); simpl in K; case K; clear K; subst a.
+  set (a := Qred y) at 1;
+  assert (K := canon (Q2Qc y)); simpl in K; case K; clear K; subst a.
+  fold (x - Qred y)%Q (x - Qred r)%Q.
+  destruct (Qabs_diff_Qle_condition x (Qred y) (Qred r)) as [A B].
+  split.
+  + clear B; rewrite !Qred_le. auto.
+  + clear A; rewrite !Qred_le. auto.
+Qed.
+
+Lemma Qcabs_null x : [x] = 0 -> x = 0.
+Proof.
+  intros H.
+  destruct (proj1 (Qcabs_Qcle_condition x 0)) as [A B].
+  + rewrite H; apply Qcle_refl.
+  + apply Qcle_antisym; auto.
+Qed.
\ No newline at end of file
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index d966b050..9f9651d8 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -21,37 +21,30 @@ Bind Scope Qc_scope with Qc.
 Arguments Qcmake this%Q _.
 Open Scope Qc_scope.
 
+(** An alternative statement of [Qred q = q] via [Z.gcd] *)
+
 Lemma Qred_identity :
   forall q:Q, Z.gcd (Qnum q) (QDen q) = 1%Z -> Qred q = q.
 Proof.
-  unfold Qred; intros (a,b); simpl.
-  generalize (Z.ggcd_gcd a ('b)) (Z.ggcd_correct_divisors a ('b)).
-  intros.
-  rewrite H1 in H; clear H1.
-  destruct (Z.ggcd a ('b)) as (g,(aa,bb)); simpl in *; subst.
-  destruct H0.
-  rewrite Z.mul_1_l in H, H0.
-  subst; simpl; auto.
+  intros (a,b) H; simpl in *.
+  rewrite <- Z.ggcd_gcd in H.
+  generalize (Z.ggcd_correct_divisors a ('b)).
+  destruct Z.ggcd as (g,(aa,bb)); simpl in *; subst.
+  rewrite !Z.mul_1_l. now intros (<-,<-).
 Qed.
 
 Lemma Qred_identity2 :
   forall q:Q, Qred q = q -> Z.gcd (Qnum q) (QDen q) = 1%Z.
 Proof.
-  unfold Qred; intros (a,b); simpl.
-  generalize (Z.ggcd_gcd a ('b)) (Z.ggcd_correct_divisors a ('b)) (Z.gcd_nonneg a ('b)).
-  intros.
-  rewrite <- H; rewrite <- H in H1; clear H.
-  destruct (Z.ggcd a ('b)) as (g,(aa,bb)); simpl in *; subst.
-  injection H2; intros; clear H2.
-  destruct H0.
-  clear H0 H3.
-  destruct g as [|g|g]; destruct bb as [|bb|bb]; simpl in *; try discriminate.
-  f_equal.
-  apply Pos.mul_reg_r with bb.
-  injection H2; intros.
-  rewrite <- H0.
-  rewrite H; simpl; auto.
-  elim H1; auto.
+  intros (a,b) H; simpl in *.
+  generalize (Z.gcd_nonneg a ('b)) (Z.ggcd_correct_divisors a ('b)).
+  rewrite <- Z.ggcd_gcd.
+  destruct Z.ggcd as (g,(aa,bb)); simpl in *.
+  injection H as <- <-. intros H (_,H').
+  destruct g as [|g|g]; [ discriminate | | now elim H ].
+  destruct bb as [|b|b]; simpl in *; try discriminate.
+  injection H' as H'. f_equal.
+  apply Pos.mul_reg_r with b. now rewrite Pos.mul_1_l.
 Qed.
 
 Lemma Qred_iff : forall q:Q, Qred q = q <-> Z.gcd (Qnum q) (QDen q) = 1%Z.
@@ -61,6 +54,23 @@ Proof.
   apply Qred_identity; auto.
 Qed.
 
+(** Coercion from [Qc] to [Q] and equality *)
+
+Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'.
+Proof.
+  intros (q,hq) (q',hq') H. simpl in *.
+  assert (H' := Qred_complete _ _ H).
+  rewrite hq, hq' in H'. subst q'. f_equal.
+  apply eq_proofs_unicity. intros.  repeat decide equality.
+Qed.
+Hint Resolve Qc_is_canon.
+
+Theorem Qc_decomp: forall q q': Qc, (q:Q) = q' -> q = q'.
+Proof.
+  intros. apply Qc_is_canon. now rewrite H.
+Qed.
+
+(** [Q2Qc] : a conversion from [Q] to [Qc]. *)
 
 Lemma Qred_involutive : forall q:Q, Qred (Qred q) = Qred q.
 Proof.
@@ -71,20 +81,12 @@ Qed.
 Definition Q2Qc (q:Q) : Qc := Qcmake (Qred q) (Qred_involutive q).
 Arguments Q2Qc q%Q.
 
-Lemma Qc_is_canon : forall q q' : Qc, q == q' -> q = q'.
+Lemma Q2Qc_eq_iff (q q' : Q) : Q2Qc q = Q2Qc q' <-> q == q'.
 Proof.
-  intros (q,proof_q) (q',proof_q').
-  simpl.
-  intros H.
-  assert (H0:=Qred_complete _ _ H).
-  assert (q = q') by congruence.
-  subst q'.
-  assert (proof_q = proof_q').
-  apply eq_proofs_unicity; auto; intros.
-  repeat decide equality.
-  congruence.
+ split; intro H.
+ - now injection H as H%Qred_eq_iff.
+ - apply Qc_is_canon. simpl. now rewrite H.
 Qed.
-Hint Resolve Qc_is_canon.
 
 Notation " 0 " := (Q2Qc 0) : Qc_scope.
 Notation " 1 " := (Q2Qc 1) : Qc_scope.
@@ -107,8 +109,7 @@ Lemma Qceq_alt : forall p q, (p = q) <-> (p ?= q) = Eq.
 Proof.
   unfold Qccompare.
   intros; rewrite <- Qeq_alt.
-  split; auto.
-  intro H; rewrite H; auto with qarith.
+  split; auto. now intros <-.
 Qed.
 
 Lemma Qclt_alt : forall p q, (p<q) <-> (p?=q = Lt).
@@ -121,12 +122,12 @@ Proof.
   intros; exact (Qgt_alt p q).
 Qed.
 
-Lemma Qle_alt : forall p q, (p<=q) <-> (p?=q <> Gt).
+Lemma Qcle_alt : forall p q, (p<=q) <-> (p?=q <> Gt).
 Proof.
   intros; exact (Qle_alt p q).
 Qed.
 
-Lemma Qge_alt : forall p q, (p>=q) <-> (p?=q <> Lt).
+Lemma Qcge_alt : forall p q, (p>=q) <-> (p?=q <> Lt).
 Proof.
   intros; exact (Qge_alt p q).
 Qed.
@@ -166,7 +167,7 @@ Qed.
 
 Ltac qc := match goal with
  | q:Qc |- _ => destruct q; qc
- | _ => apply Qc_is_canon; simpl; repeat rewrite Qred_correct
+ | _ => apply Qc_is_canon; simpl; rewrite !Qred_correct
 end.
 
 Opaque Qred.
@@ -216,6 +217,18 @@ Proof.
   intros; qc; apply Qmult_assoc.
 Qed.
 
+(** [0] is absorbing for multiplication: *)
+
+Lemma Qcmult_0_l : forall n, 0*n = 0.
+Proof.
+  intros; qc; split.
+Qed.
+
+Theorem Qcmult_0_r : forall n, n*0=0.
+Proof.
+  intros; qc; rewrite Qmult_comm; split.
+Qed.
+
 (** [1] is a neutral element for multiplication: *)
 
 Lemma Qcmult_1_l : forall n, 1*n = n.
@@ -253,7 +266,7 @@ Theorem Qcmult_integral : forall x y, x*y=0 -> x=0 \/ y=0.
 Proof.
   intros.
   destruct (Qmult_integral x y); try qc; auto.
-  injection H; clear H; intros.
+  injection H as H.
   rewrite <- (Qred_correct (x*y)).
   rewrite <- (Qred_correct 0).
   rewrite H; auto with qarith.
@@ -303,7 +316,7 @@ Proof.
   apply Qcmult_1_l.
 Qed.
 
-(** Properties of order upon Q. *)
+(** Properties of order upon Qc. *)
 
 Lemma Qcle_refl : forall x, x<=x.
 Proof.
@@ -372,9 +385,11 @@ Proof.
   unfold Qcle, Qclt; intros; apply Qle_not_lt; auto.
 Qed.
 
-Lemma Qcle_lt_or_eq : forall x y, x<=y -> x<y \/ x==y.
+Lemma Qcle_lt_or_eq : forall x y, x<=y -> x<y \/ x=y.
 Proof.
-  unfold Qcle, Qclt; intros; apply Qle_lt_or_eq; auto.
+  unfold Qcle, Qclt; intros x y H.
+  destruct (Qle_lt_or_eq _ _ H); [left|right]; trivial.
+  now apply Qc_is_canon.
 Qed.
 
 (** Some decidability results about orders. *)
@@ -459,13 +474,13 @@ Proof.
   induction n; simpl; auto with qarith.
   rewrite IHn; auto with qarith.
 Qed.
-Transparent Qred.
+
 Lemma Qcpower_0 : forall n, n<>O -> 0^n = 0.
 Proof.
   destruct n; simpl.
   destruct 1; auto.
   intros.
-  now apply Qc_is_canon. 
+  now apply Qc_is_canon.
 Qed.
 
 Lemma Qcpower_pos : forall p n, 0 <= p -> 0 <= p^n.
@@ -525,16 +540,3 @@ intros.
 field.
 auto.
 Qed.
-
-
-Theorem Qc_decomp: forall x y: Qc,
-  (Qred x = x -> Qred y = y -> (x:Q) = y)-> x = y.
-Proof.
-  intros (q, Hq) (q', Hq'); simpl; intros H.
-  assert (H1 := H Hq Hq').
-  subst q'.
-  assert (Hq = Hq').
-  apply Eqdep_dec.eq_proofs_unicity; auto; intros.
-  repeat decide equality.
-  congruence.
-Qed.
diff --git a/theories/QArith/Qreduction.v b/theories/QArith/Qreduction.v
index c50c38b2..131214f5 100644
--- a/theories/QArith/Qreduction.v
+++ b/theories/QArith/Qreduction.v
@@ -93,11 +93,17 @@ Proof.
   Close Scope Z_scope.
 Qed.
 
+Lemma Qred_eq_iff q q' : Qred q = Qred q' <-> q == q'.
+Proof.
+ split.
+ - intros E. rewrite <- (Qred_correct q), <- (Qred_correct q').
+   now rewrite E.
+ - apply Qred_complete.
+Qed.
+
 Add Morphism Qred : Qred_comp.
 Proof.
-  intros q q' H.
-  rewrite (Qred_correct q); auto.
-  rewrite (Qred_correct q'); auto.
+  intros. now rewrite !Qred_correct.
 Qed.
 
 Definition Qplus' (p q : Q) := Qred (Qplus p q).
@@ -149,3 +155,13 @@ Theorem Qred_compare: forall x y,
 Proof.
   intros x y; apply Qcompare_comp; apply Qeq_sym; apply Qred_correct.
 Qed.
+
+Lemma Qred_le q q' : Qred q <= Qred q' <-> q <= q'.
+Proof.
+  now rewrite !Qle_alt, <- Qred_compare.
+Qed.
+
+Lemma Qred_lt q q' : Qred q < Qred q' <-> q < q'.
+Proof.
+  now rewrite !Qlt_alt, <- Qred_compare.
+Qed.
diff --git a/theories/QArith/vo.itarget b/theories/QArith/vo.itarget
index b3faef88..b550b471 100644
--- a/theories/QArith/vo.itarget
+++ b/theories/QArith/vo.itarget
@@ -2,6 +2,7 @@ Qabs.vo
 QArith_base.vo
 QArith.vo
 Qcanon.vo
+Qcabs.vo
 Qfield.vo
 Qpower.vo
 Qreals.vo
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index f26bac2b..379fee6f 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -389,7 +389,7 @@ Lemma Rplus_ne : forall r, r + 0 = r /\ 0 + r = r.
 Proof.
   split; ring.
 Qed.
-Hint Resolve Rplus_ne: real v62.
+Hint Resolve Rplus_ne: real.
 
 (**********)
 
@@ -425,7 +425,6 @@ Proof.
   apply (f_equal (fun v => v + r)).
 Qed.
 
-(*i Old i*)Hint Resolve Rplus_eq_compat_l: v62.
 
 (**********)
 Lemma Rplus_eq_reg_l : forall r r1 r2, r + r1 = r + r2 -> r1 = r2.
@@ -501,21 +500,21 @@ Lemma Rmult_0_r : forall r, r * 0 = 0.
 Proof.
   intro; ring.
 Qed.
-Hint Resolve Rmult_0_r: real v62.
+Hint Resolve Rmult_0_r: real.
 
 (**********)
 Lemma Rmult_0_l : forall r, 0 * r = 0.
 Proof.
   intro; ring.
 Qed.
-Hint Resolve Rmult_0_l: real v62.
+Hint Resolve Rmult_0_l: real.
 
 (**********)
 Lemma Rmult_ne : forall r, r * 1 = r /\ 1 * r = r.
 Proof.
   intro; split; ring.
 Qed.
-Hint Resolve Rmult_ne: real v62.
+Hint Resolve Rmult_ne: real.
 
 (**********)
 Lemma Rmult_1_r : forall r, r * 1 = r.
@@ -530,7 +529,6 @@ Proof.
   auto with real.
 Qed.
 
-(*i Old i*)Hint Resolve Rmult_eq_compat_l: v62.
 
 Lemma Rmult_eq_compat_r : forall r r1 r2, r1 = r2 -> r1 * r = r2 * r.
 Proof.
@@ -646,7 +644,7 @@ Lemma Ropp_0 : -0 = 0.
 Proof.
   ring.
 Qed.
-Hint Resolve Ropp_0: real v62.
+Hint Resolve Ropp_0: real.
 
 (**********)
 Lemma Ropp_eq_0_compat : forall r, r = 0 -> - r = 0.
diff --git a/theories/Reals/Ranalysis_reg.v b/theories/Reals/Ranalysis_reg.v
index 2465f039..0c27d407 100644
--- a/theories/Reals/Ranalysis_reg.v
+++ b/theories/Reals/Ranalysis_reg.v
@@ -35,7 +35,7 @@ Qed.
 
 (**********)
 Ltac intro_hyp_glob trm :=
-  match constr:trm with
+  match constr:(trm) with
     | (?X1 + ?X2)%F =>
       match goal with
         |  |- (derivable _) => intro_hyp_glob X1; intro_hyp_glob X2
@@ -55,7 +55,7 @@ Ltac intro_hyp_glob trm :=
         | _ => idtac
       end
     | (?X1 / ?X2)%F =>
-      let aux := constr:X2 in
+      let aux := constr:(X2) in
         match goal with
           | _:(forall x0:R, aux x0 <> 0) |- (derivable _) =>
             intro_hyp_glob X1; intro_hyp_glob X2
@@ -82,7 +82,7 @@ Ltac intro_hyp_glob trm :=
         | _ => idtac
       end
     | (/ ?X1)%F =>
-      let aux := constr:X1 in
+      let aux := constr:(X1) in
         match goal with
           | _:(forall x0:R, aux x0 <> 0) |- (derivable _) =>
             intro_hyp_glob X1
@@ -108,7 +108,8 @@ Ltac intro_hyp_glob trm :=
     | (pow_fct _) => idtac
     | Rabs => idtac
     | ?X1 =>
-      let p := constr:X1 in
+      let p := constr:(X1) in
+      let HYPPD := fresh "HYPPD" in
         match goal with
           | _:(derivable p) |- _ => idtac
           |  |- (derivable p) => idtac
@@ -130,7 +131,7 @@ Ltac intro_hyp_glob trm :=
 
 (**********)
 Ltac intro_hyp_pt trm pt :=
-  match constr:trm with
+  match constr:(trm) with
     | (?X1 + ?X2)%F =>
       match goal with
         |  |- (derivable_pt _ _) => intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
@@ -156,7 +157,7 @@ Ltac intro_hyp_pt trm pt :=
         | _ => idtac
       end
     | (?X1 / ?X2)%F =>
-      let aux := constr:X2 in
+      let aux := constr:(X2) in
         match goal with
           | _:(aux pt <> 0) |- (derivable_pt _ _) =>
             intro_hyp_pt X1 pt; intro_hyp_pt X2 pt
@@ -202,7 +203,7 @@ Ltac intro_hyp_pt trm pt :=
         | _ => idtac
       end
     | (/ ?X1)%F =>
-      let aux := constr:X1 in
+      let aux := constr:(X1) in
         match goal with
           | _:(aux pt <> 0) |- (derivable_pt _ _) =>
             intro_hyp_pt X1 pt
@@ -249,7 +250,8 @@ Ltac intro_hyp_pt trm pt :=
         | _ => idtac
       end
     | ?X1 =>
-      let p := constr:X1 in
+      let p := constr:(X1) in
+      let HYPPD := fresh "HYPPD" in
         match goal with
           | _:(derivable_pt p pt) |- _ => idtac
           |  |- (derivable_pt p pt) => idtac
@@ -341,8 +343,10 @@ Ltac is_diff_pt :=
     | _:(derivable_pt ?X1 ?X2) |- (derivable_pt ?X1 ?X2) =>
       assumption
     | _:(derivable ?X1) |- (derivable_pt ?X1 ?X2) =>
+      let HypDDPT := fresh "HypDDPT" in
       cut (derivable X1); [ intro HypDDPT; apply HypDDPT | assumption ]
     |  |- (True -> derivable_pt _ _) =>
+      let HypTruE := fresh "HypTruE" in
       intro HypTruE; clear HypTruE; is_diff_pt
     | _ =>
       try
@@ -411,6 +415,7 @@ Ltac is_diff_glob :=
       apply (derivable_comp X2 X1); is_diff_glob
     | _:(derivable ?X1) |- (derivable ?X1) => assumption
     |  |- (True -> derivable _) =>
+      let HypTruE := fresh "HypTruE" in
       intro HypTruE; clear HypTruE; is_diff_glob
     | _ =>
       try
@@ -490,14 +495,17 @@ Ltac is_cont_pt :=
     | _:(continuity_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) =>
       assumption
     | _:(continuity ?X1) |- (continuity_pt ?X1 ?X2) =>
+      let HypDDPT := fresh "HypDDPT" in
       cut (continuity X1); [ intro HypDDPT; apply HypDDPT | assumption ]
     | _:(derivable_pt ?X1 ?X2) |- (continuity_pt ?X1 ?X2) =>
       apply derivable_continuous_pt; assumption
     | _:(derivable ?X1) |- (continuity_pt ?X1 ?X2) =>
+      let HypDDPT := fresh "HypDDPT" in
       cut (continuity X1);
         [ intro HypDDPT; apply HypDDPT
           | apply derivable_continuous; assumption ]
     |  |- (True -> continuity_pt _ _) =>
+      let HypTruE := fresh "HypTruE" in
       intro HypTruE; clear HypTruE; is_cont_pt
     | _ =>
       try
@@ -567,6 +575,7 @@ Ltac is_cont_glob :=
       apply (continuity_comp X2 X1); try is_cont_glob || assumption
     | _:(continuity ?X1) |- (continuity ?X1) => assumption
     |  |- (True -> continuity _) =>
+      let HypTruE := fresh "HypTruE" in
       intro HypTruE; clear HypTruE; is_cont_glob
     | _:(derivable ?X1) |- (continuity ?X1) =>
       apply derivable_continuous; assumption
@@ -578,89 +587,89 @@ Ltac is_cont_glob :=
 
 (**********)
 Ltac rew_term trm :=
-  match constr:trm with
+  match constr:(trm) with
     | (?X1 + ?X2) =>
       let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
+        match constr:(p1) with
           | (fct_cte ?X3) =>
-            match constr:p2 with
+            match constr:(p2) with
               | (fct_cte ?X4) => constr:(fct_cte (X3 + X4))
-              | _ => constr:(p1 + p2)%F
+              | _ => constr:((p1 + p2)%F)
             end
-          | _ => constr:(p1 + p2)%F
+          | _ => constr:((p1 + p2)%F)
         end
     | (?X1 - ?X2) =>
       let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
+        match constr:(p1) with
           | (fct_cte ?X3) =>
-            match constr:p2 with
+            match constr:(p2) with
               | (fct_cte ?X4) => constr:(fct_cte (X3 - X4))
-              | _ => constr:(p1 - p2)%F
+              | _ => constr:((p1 - p2)%F)
             end
-          | _ => constr:(p1 - p2)%F
+          | _ => constr:((p1 - p2)%F)
         end
     | (?X1 / ?X2) =>
       let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
+        match constr:(p1) with
           | (fct_cte ?X3) =>
-            match constr:p2 with
+            match constr:(p2) with
               | (fct_cte ?X4) => constr:(fct_cte (X3 / X4))
-              | _ => constr:(p1 / p2)%F
+              | _ => constr:((p1 / p2)%F)
             end
           | _ =>
-            match constr:p2 with
-              | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F
-              | _ => constr:(p1 / p2)%F
+            match constr:(p2) with
+              | (fct_cte ?X4) => constr:((p1 * fct_cte (/ X4))%F)
+              | _ => constr:((p1 / p2)%F)
             end
         end
     | (?X1 * / ?X2) =>
       let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
+        match constr:(p1) with
           | (fct_cte ?X3) =>
-            match constr:p2 with
+            match constr:(p2) with
               | (fct_cte ?X4) => constr:(fct_cte (X3 / X4))
-              | _ => constr:(p1 / p2)%F
+              | _ => constr:((p1 / p2)%F)
             end
           | _ =>
-            match constr:p2 with
-              | (fct_cte ?X4) => constr:(p1 * fct_cte (/ X4))%F
-              | _ => constr:(p1 / p2)%F
+            match constr:(p2) with
+              | (fct_cte ?X4) => constr:((p1 * fct_cte (/ X4))%F)
+              | _ => constr:((p1 / p2)%F)
             end
         end
     | (?X1 * ?X2) =>
       let p1 := rew_term X1 with p2 := rew_term X2 in
-        match constr:p1 with
+        match constr:(p1) with
           | (fct_cte ?X3) =>
-            match constr:p2 with
+            match constr:(p2) with
               | (fct_cte ?X4) => constr:(fct_cte (X3 * X4))
-              | _ => constr:(p1 * p2)%F
+              | _ => constr:((p1 * p2)%F)
             end
-          | _ => constr:(p1 * p2)%F
+          | _ => constr:((p1 * p2)%F)
         end
     | (- ?X1) =>
       let p := rew_term X1 in
-        match constr:p with
+        match constr:(p) with
           | (fct_cte ?X2) => constr:(fct_cte (- X2))
-          | _ => constr:(- p)%F
+          | _ => constr:((- p)%F)
         end
     | (/ ?X1) =>
       let p := rew_term X1 in
-        match constr:p with
+        match constr:(p) with
           | (fct_cte ?X2) => constr:(fct_cte (/ X2))
-          | _ => constr:(/ p)%F
+          | _ => constr:((/ p)%F)
         end
-    | (?X1 AppVar) => constr:X1
+    | (?X1 AppVar) => constr:(X1)
     | (?X1 ?X2) =>
       let p := rew_term X2 in
-        match constr:p with
+        match constr:(p) with
           | (fct_cte ?X3) => constr:(fct_cte (X1 X3))
           | _ => constr:(comp X1 p)
         end
-    | AppVar => constr:id
+    | AppVar => constr:(id)
     | (AppVar ^ ?X1) => constr:(pow_fct X1)
     | (?X1 ^ ?X2) =>
       let p := rew_term X1 in
-        match constr:p with
+        match constr:(p) with
           | (fct_cte ?X3) => constr:(fct_cte (pow_fct X2 X3))
           | _ => constr:(comp (pow_fct X2) p)
         end
@@ -669,7 +678,7 @@ Ltac rew_term trm :=
 
 (**********)
 Ltac deriv_proof trm pt :=
-  match constr:trm with
+  match constr:(trm) with
     | (?X1 + ?X2)%F =>
       let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
         constr:(derivable_pt_plus X1 X2 pt p1 p2)
@@ -684,14 +693,14 @@ Ltac deriv_proof trm pt :=
         | id:(?X2 pt <> 0) |- _ =>
           let p1 := deriv_proof X1 pt with p2 := deriv_proof X2 pt in
             constr:(derivable_pt_div X1 X2 pt p1 p2 id)
-        | _ => constr:False
+        | _ => constr:(False)
       end
     | (/ ?X1)%F =>
       match goal with
         | id:(?X1 pt <> 0) |- _ =>
           let p1 := deriv_proof X1 pt in
             constr:(derivable_pt_inv X1 pt p1 id)
-        | _ => constr:False
+        | _ => constr:(False)
       end
     | (comp ?X1 ?X2) =>
       let pt_f1 := eval cbv beta in (X2 pt) in
@@ -710,21 +719,21 @@ Ltac deriv_proof trm pt :=
     | sqrt =>
       match goal with
         | id:(0 < pt) |- _ => constr:(derivable_pt_sqrt pt id)
-        | _ => constr:False
+        | _ => constr:(False)
       end
     | (fct_cte ?X1) => constr:(derivable_pt_const X1 pt)
     | ?X1 =>
-      let aux := constr:X1 in
+      let aux := constr:(X1) in
         match goal with
-          | id:(derivable_pt aux pt) |- _ => constr:id
+          | id:(derivable_pt aux pt) |- _ => constr:(id)
           | id:(derivable aux) |- _ => constr:(id pt)
-          | _ => constr:False
+          | _ => constr:(False)
         end
   end.
 
 (**********)
 Ltac simplify_derive trm pt :=
-  match constr:trm with
+  match constr:(trm) with
     | (?X1 + ?X2)%F =>
       try rewrite derive_pt_plus; simplify_derive X1 pt;
         simplify_derive X2 pt
@@ -753,7 +762,7 @@ Ltac simplify_derive trm pt :=
     | Rsqr => try rewrite derive_pt_Rsqr
     | sqrt => try rewrite derive_pt_sqrt
     | ?X1 =>
-      let aux := constr:X1 in
+      let aux := constr:(X1) in
         match goal with
           | id:(derive_pt aux pt ?X2 = _),H:(derivable aux) |- _ =>
             try replace (derive_pt aux pt (H pt)) with (derive_pt aux pt X2);
diff --git a/theories/Reals/Raxioms.v b/theories/Reals/Raxioms.v
index 9d55e4e6..9fbda92a 100644
--- a/theories/Reals/Raxioms.v
+++ b/theories/Reals/Raxioms.v
@@ -32,7 +32,7 @@ Hint Resolve Rplus_assoc: real.
 
 (**********)
 Axiom Rplus_opp_r : forall r:R, r + - r = 0.
-Hint Resolve Rplus_opp_r: real v62.
+Hint Resolve Rplus_opp_r: real.
 
 (**********)
 Axiom Rplus_0_l : forall r:R, 0 + r = r.
@@ -44,11 +44,11 @@ Hint Resolve Rplus_0_l: real.
 
 (**********)
 Axiom Rmult_comm : forall r1 r2:R, r1 * r2 = r2 * r1.
-Hint Resolve Rmult_comm: real v62.
+Hint Resolve Rmult_comm: real.
 
 (**********)
 Axiom Rmult_assoc : forall r1 r2 r3:R, r1 * r2 * r3 = r1 * (r2 * r3).
-Hint Resolve Rmult_assoc: real v62.
+Hint Resolve Rmult_assoc: real.
 
 (**********)
 Axiom Rinv_l : forall r:R, r <> 0 -> / r * r = 1.
@@ -69,7 +69,7 @@ Hint Resolve R1_neq_R0: real.
 (**********)
 Axiom
   Rmult_plus_distr_l : forall r1 r2 r3:R, r1 * (r2 + r3) = r1 * r2 + r1 * r3.
-Hint Resolve Rmult_plus_distr_l: real v62.
+Hint Resolve Rmult_plus_distr_l: real.
 
 (*********************************************************)
 (** *    Order axioms                                    *)
diff --git a/theories/Reals/Sqrt_reg.v b/theories/Reals/Sqrt_reg.v
index 10527442..d43baee8 100644
--- a/theories/Reals/Sqrt_reg.v
+++ b/theories/Reals/Sqrt_reg.v
@@ -339,7 +339,7 @@ Proof.
   rewrite <- H1; rewrite sqrt_0; unfold Rminus; rewrite Ropp_0;
     rewrite Rplus_0_r; rewrite <- H1 in H5; unfold Rminus in H5;
       rewrite Ropp_0 in H5; rewrite Rplus_0_r in H5.
-  destruct (Rcase_abs x0) as [Hlt|Hgt]_eqn:Heqs.
+  destruct (Rcase_abs x0) as [Hlt|Hgt] eqn:Heqs.
   unfold sqrt. rewrite Heqs.
   rewrite Rabs_R0; apply H2.
   rewrite Rabs_right.
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 220cebea..fe8a96ac 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -36,7 +36,7 @@ Section Properties.
   Section Clos_Refl_Trans.
 
     Local Notation "R *" := (clos_refl_trans R)
-      (at level 8, left associativity, format "R *").
+      (at level 8, no associativity, format "R *").
 
     (** Correctness of the reflexive-transitive closure operator *)
 
diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index b6005b9d..9c98879c 100644
--- a/theories/Relations/Relation_Definitions.v
+++ b/theories/Relations/Relation_Definitions.v
@@ -66,10 +66,10 @@ Section Relation_Definition.
 
 End Relation_Definition.
 
-Hint Unfold reflexive transitive antisymmetric symmetric: sets v62.
+Hint Unfold reflexive transitive antisymmetric symmetric: sets.
 
 Hint Resolve Build_preorder Build_order Build_equivalence Build_PER
   preord_refl preord_trans ord_refl ord_trans ord_antisym equiv_refl
-  equiv_trans equiv_sym per_sym per_trans: sets v62.
+  equiv_trans equiv_sym per_sym per_trans: sets.
 
-Hint Unfold inclusion same_relation commut: sets v62.
+Hint Unfold inclusion same_relation commut: sets.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index ffd682d6..88239475 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -226,9 +226,9 @@ Section Lexicographic_Exponentiation.
 
 End Lexicographic_Exponentiation.
 
-Hint Unfold transp union: sets v62.
-Hint Resolve t_step rt_step rt_refl rst_step rst_refl: sets v62.
-Hint Immediate rst_sym: sets v62.
+Hint Unfold transp union: sets.
+Hint Resolve t_step rt_step rt_refl rst_step rst_refl: sets.
+Hint Immediate rst_sym: sets.
 
 (* begin hide *)
 (* Compatibility *)
diff --git a/theories/Sets/Classical_sets.v b/theories/Sets/Classical_sets.v
index 8a4bb9f4..837437a2 100644
--- a/theories/Sets/Classical_sets.v
+++ b/theories/Sets/Classical_sets.v
@@ -122,4 +122,4 @@ Section Ensembles_classical.
 End Ensembles_classical.
 
  Hint Resolve Strict_super_set_contains_new_element Subtract_intro
-  not_SIncl_empty: sets v62.
+  not_SIncl_empty: sets.
diff --git a/theories/Sets/Constructive_sets.v b/theories/Sets/Constructive_sets.v
index 8d2344f9..6291248e 100644
--- a/theories/Sets/Constructive_sets.v
+++ b/theories/Sets/Constructive_sets.v
@@ -141,4 +141,4 @@ End Ensembles_facts.
 Hint Resolve Singleton_inv Singleton_intro Add_intro1 Add_intro2
   Intersection_inv Couple_inv Setminus_intro Strict_Included_intro
   Strict_Included_strict Noone_in_empty Inhabited_not_empty Add_not_Empty
-  not_Empty_Add Inhabited_add Included_Empty: sets v62.
+  not_Empty_Add Inhabited_add Included_Empty: sets.
diff --git a/theories/Sets/Ensembles.v b/theories/Sets/Ensembles.v
index 8f579214..0fefb354 100644
--- a/theories/Sets/Ensembles.v
+++ b/theories/Sets/Ensembles.v
@@ -90,9 +90,8 @@ Section Ensembles.
 
 End Ensembles.
 
-Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets
-  v62.
+Hint Unfold In Included Same_set Strict_Included Add Setminus Subtract: sets.
 
 Hint Resolve Union_introl Union_intror Intersection_intro In_singleton
   Couple_l Couple_r Triple_l Triple_m Triple_r Disjoint_intro
-  Extensionality_Ensembles: sets v62.
+  Extensionality_Ensembles: sets.
diff --git a/theories/Sets/Finite_sets.v b/theories/Sets/Finite_sets.v
index f38dd6fd..edbc1efe 100644
--- a/theories/Sets/Finite_sets.v
+++ b/theories/Sets/Finite_sets.v
@@ -43,8 +43,8 @@ Section Ensembles_finis.
 
 End Ensembles_finis.
 
-Hint Resolve Empty_is_finite Union_is_finite: sets v62.
-Hint Resolve card_empty card_add: sets v62.
+Hint Resolve Empty_is_finite Union_is_finite: sets.
+Hint Resolve card_empty card_add: sets.
 
 Require Import Constructive_sets.
 
diff --git a/theories/Sets/Image.v b/theories/Sets/Image.v
index 34ea857d..e74ef41e 100644
--- a/theories/Sets/Image.v
+++ b/theories/Sets/Image.v
@@ -200,4 +200,4 @@ Section Image.
 
 End Image.
 
-Hint Resolve Im_def image_empty finite_image: sets v62.
+Hint Resolve Im_def image_empty finite_image: sets.
diff --git a/theories/Sets/Multiset.v b/theories/Sets/Multiset.v
index ec38b892..42d0c76d 100644
--- a/theories/Sets/Multiset.v
+++ b/theories/Sets/Multiset.v
@@ -187,7 +187,7 @@ End multiset_defs.
 
 Unset Implicit Arguments.
 
-Hint Unfold meq multiplicity: v62 datatypes.
+Hint Unfold meq multiplicity: datatypes.
 Hint Resolve munion_empty_right munion_comm munion_ass meq_left meq_right
-  munion_empty_left: v62 datatypes.
-Hint Immediate meq_sym: v62 datatypes.
+  munion_empty_left: datatypes.
+Hint Immediate meq_sym: datatypes.
diff --git a/theories/Sets/Partial_Order.v b/theories/Sets/Partial_Order.v
index 3610ebce..335fec5b 100644
--- a/theories/Sets/Partial_Order.v
+++ b/theories/Sets/Partial_Order.v
@@ -51,8 +51,8 @@ Section Partial_orders.
 
 End Partial_orders.
 
-Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets v62.
-Hint Resolve Definition_of_covers: sets v62.
+Hint Unfold Carrier_of Rel_of Strict_Rel_of: sets.
+Hint Resolve Definition_of_covers: sets.
 
 
 Section Partial_order_facts.
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index d636e046..7c2435da 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -175,14 +175,14 @@ Qed.
 
 End The_power_set_partial_order.
 
-Hint Resolve Empty_set_minimal: sets v62.
-Hint Resolve Power_set_Inhabited: sets v62.
-Hint Resolve Inclusion_is_an_order: sets v62.
-Hint Resolve Inclusion_is_transitive: sets v62.
-Hint Resolve Union_minimal: sets v62.
-Hint Resolve Union_increases_l: sets v62.
-Hint Resolve Union_increases_r: sets v62.
-Hint Resolve Intersection_decreases_l: sets v62.
-Hint Resolve Intersection_decreases_r: sets v62.
-Hint Resolve Empty_set_is_Bottom: sets v62.
-Hint Resolve Strict_inclusion_is_transitive: sets v62.
+Hint Resolve Empty_set_minimal: sets.
+Hint Resolve Power_set_Inhabited: sets.
+Hint Resolve Inclusion_is_an_order: sets.
+Hint Resolve Inclusion_is_transitive: sets.
+Hint Resolve Union_minimal: sets.
+Hint Resolve Union_increases_l: sets.
+Hint Resolve Union_increases_r: sets.
+Hint Resolve Intersection_decreases_l: sets.
+Hint Resolve Intersection_decreases_r: sets.
+Hint Resolve Empty_set_is_Bottom: sets.
+Hint Resolve Strict_inclusion_is_transitive: sets.
diff --git a/theories/Sets/Powerset_Classical_facts.v b/theories/Sets/Powerset_Classical_facts.v
index 09c90506..e802beac 100644
--- a/theories/Sets/Powerset_Classical_facts.v
+++ b/theories/Sets/Powerset_Classical_facts.v
@@ -90,7 +90,7 @@ Section Sets_as_an_algebra.
     apply Subtract_intro; auto with sets.
     red; intro H'1; apply H'; rewrite H'1; auto with sets.
   Qed.
-  Hint Resolve incl_soustr_add_r: sets v62.
+  Hint Resolve incl_soustr_add_r: sets.
 
   Lemma add_soustr_2 :
     forall (X:Ensemble U) (x:U),
@@ -328,9 +328,9 @@ Section Sets_as_an_algebra.
 
 End Sets_as_an_algebra.
 
-Hint Resolve incl_soustr_in: sets v62.
-Hint Resolve incl_soustr: sets v62.
-Hint Resolve incl_soustr_add_l: sets v62.
-Hint Resolve incl_soustr_add_r: sets v62.
-Hint Resolve add_soustr_1 add_soustr_2: sets v62.
-Hint Resolve add_soustr_xy: sets v62.
+Hint Resolve incl_soustr_in: sets.
+Hint Resolve incl_soustr: sets.
+Hint Resolve incl_soustr_add_l: sets.
+Hint Resolve incl_soustr_add_r: sets.
+Hint Resolve add_soustr_1 add_soustr_2: sets.
+Hint Resolve add_soustr_xy: sets.
diff --git a/theories/Sets/Powerset_facts.v b/theories/Sets/Powerset_facts.v
index 63e84199..e9696a1c 100644
--- a/theories/Sets/Powerset_facts.v
+++ b/theories/Sets/Powerset_facts.v
@@ -254,5 +254,5 @@ Section Sets_as_an_algebra.
 End Sets_as_an_algebra.
 
 Hint Resolve Empty_set_zero Empty_set_zero' Union_associative Union_add
-  singlx incl_add: sets v62.
+  singlx incl_add: sets.
 
diff --git a/theories/Sets/Relations_1.v b/theories/Sets/Relations_1.v
index de96fa56..45fb8134 100644
--- a/theories/Sets/Relations_1.v
+++ b/theories/Sets/Relations_1.v
@@ -60,6 +60,6 @@ Section Relations_1.
 
 End Relations_1.
 Hint Unfold Reflexive Transitive Antisymmetric Symmetric contains
-  same_relation: sets v62.
+  same_relation: sets.
 Hint Resolve Definition_of_preorder Definition_of_order
-  Definition_of_equivalence Definition_of_PER: sets v62.
+  Definition_of_equivalence Definition_of_PER: sets.
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index f1026e31..1e0b83fe 100644
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.v
@@ -48,7 +48,7 @@ Definition Strongly_confluent : Prop :=
 
 End Relations_2.
 
-Hint Resolve Rstar_0: sets v62.
-Hint Resolve Rstar1_0: sets v62.
-Hint Resolve Rstar1_1: sets v62.
-Hint Resolve Rplus_0: sets v62.
+Hint Resolve Rstar_0: sets.
+Hint Resolve Rstar1_0: sets.
+Hint Resolve Rstar1_1: sets.
+Hint Resolve Rplus_0: sets.
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index 92b29988..c05b5ee7 100644
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -51,10 +51,10 @@ Section Relations_3.
    Definition Noetherian : Prop := forall x:U, noetherian x.
 
 End Relations_3.
-Hint Unfold coherent: sets v62.
-Hint Unfold locally_confluent: sets v62.
-Hint Unfold confluent: sets v62.
-Hint Unfold Confluent: sets v62.
-Hint Resolve definition_of_noetherian: sets v62.
-Hint Unfold Noetherian: sets v62.
+Hint Unfold coherent: sets.
+Hint Unfold locally_confluent: sets.
+Hint Unfold confluent: sets.
+Hint Unfold Confluent: sets.
+Hint Resolve definition_of_noetherian: sets.
+Hint Unfold Noetherian: sets.
 
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index e159efa8..44f8ff6a 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -318,10 +318,10 @@ Lemma Permutation_length_2_inv :
 Proof.
   intros a1 a2 l H; remember [a1;a2] as m in H.
   revert a1 a2 Heqm.
-  induction H; intros; try (injection Heqm; intros; subst; clear Heqm);
+  induction H; intros; try (injection Heqm as ? ?; subst);
     discriminate || (try tauto).
   apply Permutation_length_1_inv in H as ->; left; auto.
-  apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as ();
+  apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as [];
     auto.
 Qed.
 
diff --git a/theories/Strings/Ascii.v b/theories/Strings/Ascii.v
index 97cb746f..55a533c5 100644
--- a/theories/Strings/Ascii.v
+++ b/theories/Strings/Ascii.v
@@ -40,7 +40,7 @@ Defined.
 
 (** * Conversion between natural numbers modulo 256 and ascii characters *)
 
-(** Auxillary function that turns a positive into an ascii by
+(** Auxiliary function that turns a positive into an ascii by
    looking at the last 8 bits, ie z mod 2^8 *)
 
 Definition ascii_of_pos : positive -> ascii :=
diff --git a/theories/Strings/String.v b/theories/Strings/String.v
index 943bb48e..451b65cb 100644
--- a/theories/Strings/String.v
+++ b/theories/Strings/String.v
@@ -83,7 +83,7 @@ intros H; generalize (H 0); simpl; intros H1; inversion H1.
 case (Rec s).
 intros H0; rewrite H0; auto.
 intros n; exact (H (S n)).
-intros H; injection H; intros H1 H2 n; case n; auto.
+intros H; injection H as H1 H2.
 rewrite H2; trivial.
 rewrite H1; auto.
 Qed.
@@ -238,14 +238,14 @@ intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl;
  auto.
 intros n; case n; simpl; auto.
 intros m s1; case s1; simpl; auto.
-intros H; injection H; intros H1; rewrite <- H1; auto.
+intros H; injection H as <-; auto.
 intros; discriminate.
 intros; discriminate.
 intros b s2' Rec n m s1.
 case n; simpl; auto.
 generalize (prefix_correct s1 (String b s2'));
  case (prefix s1 (String b s2')).
-intros H0 H; injection H; intros H1; rewrite <- H1; auto.
+intros H0 H; injection H as <-; auto.
 case H0; simpl; auto.
 case m; simpl; auto.
 case (index 0 s1 s2'); intros; discriminate.
@@ -271,7 +271,7 @@ intros n m s1 s2; generalize n m s1; clear n m s1; elim s2; simpl;
  auto.
 intros n; case n; simpl; auto.
 intros m s1; case s1; simpl; auto.
-intros H; injection H; intros H1; rewrite <- H1.
+intros H; injection H as <-.
 intros p H0 H2; inversion H2.
 intros; discriminate.
 intros; discriminate.
@@ -279,7 +279,7 @@ intros b s2' Rec n m s1.
 case n; simpl; auto.
 generalize (prefix_correct s1 (String b s2'));
  case (prefix s1 (String b s2')).
-intros H0 H; injection H; intros H1; rewrite <- H1; auto.
+intros H0 H; injection H as <-; auto.
 intros p H2 H3; inversion H3.
 case m; simpl; auto.
 case (index 0 s1 s2'); intros; discriminate.
diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v
index 954d3df2..0115d8a5 100644
--- a/theories/Structures/OrdersFacts.v
+++ b/theories/Structures/OrdersFacts.v
@@ -434,21 +434,21 @@ Lemma eqb_compare x y :
  (x =? y) = match compare x y with Eq => true | _ => false end.
 Proof.
 apply eq_true_iff_eq. rewrite eqb_eq, <- compare_eq_iff.
-destruct compare; now split.
+now destruct compare.
 Qed.
 
 Lemma ltb_compare x y :
  (x <? y) = match compare x y with Lt => true | _ => false end.
 Proof.
 apply eq_true_iff_eq. rewrite ltb_lt, <- compare_lt_iff.
-destruct compare; now split.
+now destruct compare.
 Qed.
 
 Lemma leb_compare x y :
  (x <=? y) = match compare x y with Gt => false | _ => true end.
 Proof.
 apply eq_true_iff_eq. rewrite leb_le, <- compare_le_iff.
-destruct compare; split; try easy. now destruct 1.
+now destruct compare.
 Qed.
 
 End BoolOrderFacts.
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 45c13e5c..1f8b76cb 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -30,7 +30,7 @@ Inductive t A : nat -> Type :=
   |nil : t A 0
   |cons : forall (h:A) (n:nat), t A n -> t A (S n).
 
-Local Notation "[]" := (nil _).
+Local Notation "[ ]" := (nil _) (format "[ ]").
 Local Notation "h :: t" := (cons _ h _ t) (at level 60, right associativity).
 
 Section SCHEMES.
@@ -102,7 +102,7 @@ Definition const {A} (a:A) := nat_rect _ [] (fun n x => cons _ a n x).
 
 Computational behavior of this function should be the same as
 ocaml function. *)
-Definition nth {A} := 
+Definition nth {A} :=
 fix nth_fix {m} (v' : t A m) (p : Fin.t m) {struct v'} : A :=
 match p in Fin.t m' return t A m' -> A with
  |Fin.F1 => caseS (fun n v' => A) (fun h n t => h)
@@ -293,12 +293,14 @@ Eval cbv delta beta in fold_right (fun h H => Datatypes.cons h H) v Datatypes.ni
 End VECTORLIST.
 
 Module VectorNotations.
-Notation "[]" := [] : vector_scope.
+Delimit Scope vector_scope with vector.
+Notation "[ ]" := [] (format "[ ]") : vector_scope.
+Notation "[]" := [] (compat "8.5") : vector_scope.
 Notation "h :: t" := (h :: t) (at level 60, right associativity)
   : vector_scope.
-Notation " [ x ] " := (x :: []) : vector_scope.
-Notation " [ x ; .. ; y ] " := (cons _ x _ .. (cons _ y _ (nil _)) ..) : vector_scope
-.
+Notation "[ x ]" := (x :: []) : vector_scope.
+Notation "[ x ; y ; .. ; z ]" := (cons _ x _ (cons _ y _ .. (cons _ z _ (nil _)) ..)) : vector_scope.
+Notation "[ x ; .. ; y ]" := (cons _ x _ .. (cons _ y _ (nil _)) ..) (compat "8.4") : vector_scope.
 Notation "v [@ p ]" := (nth v p) (at level 1, format "v [@ p ]") : vector_scope.
 Open Scope vector_scope.
 End VectorNotations.
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 992263cb..d90f9956 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -75,7 +75,7 @@ Section Wf_Lexicographic_Exponentiation.
   Proof.
     intros.
     inversion H.
-    - apply app_cons_not_nil in H1 as ().
+    - apply app_cons_not_nil in H1 as [].
     - assert (x ++ [a] = [x0]) by auto with sets.
       apply app_eq_unit in H0 as [(->, _)| (_, [=])].
       auto using d_nil.
@@ -98,7 +98,7 @@ Section Wf_Lexicographic_Exponentiation.
       destruct (app_inj_tail (l ++ [y]) ([] ++ [b]) _ _ H0) as ((?, <-)%app_inj_tail, <-).
       inversion H1; subst; [ apply rt_step; assumption | apply rt_refl ].
     - inversion H0.
-      + apply app_cons_not_nil in H3 as ().
+      + apply app_cons_not_nil in H3 as [].
       + rewrite app_comm_cons in H0, H1. apply desc_prefix in H0.
         pose proof (H x0 b H0).
         apply rt_trans with (y := x0); auto with sets.
@@ -145,7 +145,7 @@ Section Wf_Lexicographic_Exponentiation.
           pose proof H0 as H0'.
           apply app_inj_tail in H0' as (_, ->).
           rewrite app_assoc_reverse in H0.
-          apply Hind in H0 as ().
+          apply Hind in H0 as [].
           split.
           assumption.
           apply d_conc; auto with sets.
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 4b8447f4..b2ada2f9 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -44,14 +44,11 @@ Section WfLexicographic_Product.
     apply H2.
     auto with sets.
 
-    injection H1.
-    destruct 2.
-    injection H3.
-    destruct 2; auto with sets.
+    injection H1 as <- _.
+    injection H3 as <- _; auto with sets.
 
     rewrite <- H1.
-    injection H3; intros _ Hx1.
-    subst x1.
+    injection H3 as -> H3.
     apply IHAcc0.
     elim inj_pair2 with A B x y' x0; assumption.
   Defined.
diff --git a/theories/ZArith/Int.v b/theories/ZArith/Int.v
index d210792f..72021f2e 100644
--- a/theories/ZArith/Int.v
+++ b/theories/ZArith/Int.v
@@ -225,11 +225,11 @@ Module MoreInt (Import I:Int).
   (** [int] to [ExprI] *)
 
   Ltac i2ei trm :=
-    match constr:trm with
-      | 0 => constr:EI0
-      | 1 => constr:EI1
-      | 2 => constr:EI2
-      | 3 => constr:EI3
+    match constr:(trm) with
+      | 0 => constr:(EI0)
+      | 1 => constr:(EI1)
+      | 2 => constr:(EI2)
+      | 3 => constr:(EI3)
       | ?x + ?y => let ex := i2ei x with ey := i2ei y in constr:(EIadd ex ey)
       | ?x - ?y => let ex := i2ei x with ey := i2ei y in constr:(EIsub ex ey)
       | ?x * ?y => let ex := i2ei x with ey := i2ei y in constr:(EImul ex ey)
@@ -241,7 +241,7 @@ Module MoreInt (Import I:Int).
   (** [Z] to [ExprZ] *)
 
     with z2ez trm :=
-    match constr:trm with
+    match constr:(trm) with
       | (?x + ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZadd ex ey)
       | (?x - ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZsub ex ey)
       | (?x * ?y)%Z => let ex := z2ez x with ey := z2ez y in constr:(EZmul ex ey)
@@ -254,7 +254,7 @@ Module MoreInt (Import I:Int).
   (** [Prop] to [ExprP] *)
 
   Ltac p2ep trm :=
-    match constr:trm with
+    match constr:(trm) with
       | (?x <-> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPequiv ex ey)
       | (?x -> ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPimpl ex ey)
       | (?x /\ ?y) => let ex := p2ep x with ey := p2ep y in constr:(EPand ex ey)
@@ -451,4 +451,8 @@ Module Z_as_Int <: Int.
   Lemma i2z_ltb n p : ltb n p = Z.ltb (i2z n) (i2z p).
   Proof. reflexivity. Qed.
 
+  (** Compatibility notations for Coq v8.4 *)
+  Notation plus := add (compat "8.4").
+  Notation minus := sub (compat "8.4").
+  Notation mult := mul (compat "8.4").
 End Z_as_Int.
diff --git a/theories/ZArith/Zsqrt_compat.v b/theories/ZArith/Zsqrt_compat.v
index b80eb445..f4baba19 100644
--- a/theories/ZArith/Zsqrt_compat.v
+++ b/theories/ZArith/Zsqrt_compat.v
@@ -30,12 +30,12 @@ Local Open Scope Z_scope.
 Ltac compute_POS :=
   match goal with
     |  |- context [(Zpos (xI ?X1))] =>
-      match constr:X1 with
+      match constr:(X1) with
 	| context [1%positive] => fail 1
 	| _ => rewrite (Pos2Z.inj_xI X1)
       end
     |  |- context [(Zpos (xO ?X1))] =>
-      match constr:X1 with
+      match constr:(X1) with
 	| context [1%positive] => fail 1
 	| _ => rewrite (Pos2Z.inj_xO X1)
       end
diff --git a/theories/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index 1ac00bdd..90754af3 100644
--- a/theories/ZArith/Zwf.v
+++ b/theories/ZArith/Zwf.v
@@ -56,7 +56,7 @@ Section wf_proof.
 
 End wf_proof.
 
-Hint Resolve Zwf_well_founded: datatypes v62.
+Hint Resolve Zwf_well_founded: datatypes.
 
 
 (** We also define the other family of relations:
@@ -88,4 +88,4 @@ Section wf_proof_up.
 
 End wf_proof_up.
 
-Hint Resolve Zwf_up_well_founded: datatypes v62.
+Hint Resolve Zwf_up_well_founded: datatypes.
diff --git a/theories/theories.itarget b/theories/theories.itarget
deleted file mode 100644
index aacab2d9..00000000
--- a/theories/theories.itarget
+++ /dev/null
@@ -1,25 +0,0 @@
-Arith/vo.otarget
-Bool/vo.otarget
-Classes/vo.otarget
-Compat/vo.otarget
-FSets/vo.otarget
-MSets/vo.otarget
-Structures/vo.otarget
-Init/vo.otarget
-Lists/vo.otarget
-Vectors/vo.otarget
-Logic/vo.otarget
-PArith/vo.otarget
-NArith/vo.otarget
-Numbers/vo.otarget
-Program/vo.otarget
-QArith/vo.otarget
-Reals/vo.otarget
-Relations/vo.otarget
-Setoids/vo.otarget
-Sets/vo.otarget
-Sorting/vo.otarget
-Strings/vo.otarget
-Unicode/vo.otarget
-Wellfounded/vo.otarget
-ZArith/vo.otarget