Remove v62 from stdlib.

This old compatibility hint database can be safely removed
now that coq-contribs do not depend on it anymore.

35 files changed, 155 insertions, 161 deletions

diff --git a/theories/Arith/Between.v b/theories/Arith/Between.v
index f998e8619..58d3a2b38 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 206fc0ab5..f998c19fc 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 dfd576946..67c94fdf6 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 ceb91187b..0fbcec572 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 f824ee6fb..bfc2b91a9 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 65534b2e3..49152549a 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 bc3a318cf..1fc8f7907 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 965812432..a173efc10 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/Plus.v b/theories/Arith/Plus.v
index 3b823da6f..600e5e518 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 721ab6932..06096c66a 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 11f3d1d6f..4257b4bc1 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/Init/Logic_Type.v b/theories/Init/Logic_Type.v
index 4a5f2ad69..4536dfc0f 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/Peano.v b/theories/Init/Peano.v
index 3749baf61..6c4a63501 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/Specif.v b/theories/Init/Specif.v
index d1038186e..9fc00e80c 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -299,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/Lists/List.v b/theories/Lists/List.v
index bf21ffb47..30f1dec22 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -340,11 +340,11 @@ Section Facts.
 
 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.
 
 
 
@@ -1544,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.
 
 
 (******************************)
@@ -1613,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.
 
 
 (**************************************)
@@ -2365,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/Streams.v b/theories/Lists/Streams.v
index 7ec3d2503..1c302b22f 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/Eqdep.v b/theories/Logic/Eqdep.v
index f3a2783e1..5ef86b8e7 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/Reals/RIneq.v b/theories/Reals/RIneq.v
index f26bac2bb..379fee6f4 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/Raxioms.v b/theories/Reals/Raxioms.v
index 9d55e4e63..9fbda92a2 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/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index b6005b9d1..9c98879ce 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 ffd682d62..88239475c 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 8a4bb9f42..837437a22 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 8d2344f93..6291248eb 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 8f579214a..0fefb354b 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 f38dd6fdf..edbc1efec 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 34ea857d1..e74ef41e4 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 ec38b8923..42d0c76dc 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 3610ebce6..335fec5b0 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 d636e0468..7c2435da0 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 09c90506b..e802beac9 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 63e84199d..e9696a1ca 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 de96fa560..45fb8134c 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 f1026e31a..1e0b83fe5 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 92b299885..c05b5ee76 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/ZArith/Zwf.v b/theories/ZArith/Zwf.v
index 1ac00bddd..90754af3b 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.