Remove v62 from stdlib.

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

9 files changed, 67 insertions, 67 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 *)