Merge branch 'v8.6'

2 files changed, 9 insertions, 11 deletions

diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index f26bac2bb4..379fee6f49 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 9d55e4e639..9fbda92a2f 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                                    *)