6 files changed, 23 insertions, 30 deletions
diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v
index 5dcd6d840d..a69cf0957c 100644
--- a/plugins/ring/LegacyNArithRing.v
+++ b/plugins/ring/LegacyNArithRing.v
@@ -22,23 +22,22 @@ Definition Neq (n m:N) :=
 
 Lemma Neq_prop : forall n m:N, Is_true (Neq n m) -> n = m.
   intros n m H; unfold Neq in H.
-  apply Ncompare_Eq_eq.
+  apply N.compare_eq.
   destruct (n ?= m)%N; [ reflexivity | contradiction | contradiction ].
 Qed.
 
-Definition NTheory : Semi_Ring_Theory Nplus Nmult 1%N 0%N Neq.
+Definition NTheory : Semi_Ring_Theory N.add N.mul 1%N 0%N Neq.
   split.
-    apply Nplus_comm.
-    apply Nplus_assoc.
-    apply Nmult_comm.
-    apply Nmult_assoc.
-    apply Nplus_0_l.
-    apply Nmult_1_l.
-    apply Nmult_0_l.
-    apply Nmult_plus_distr_r.
-(*    apply Nplus_reg_l.*)
+    apply N.add_comm.
+    apply N.add_assoc.
+    apply N.mul_comm.
+    apply N.mul_assoc.
+    apply N.add_0_l.
+    apply N.mul_1_l.
+    apply N.mul_0_l.
+    apply N.mul_add_distr_r.
     apply Neq_prop.
 Qed.
 
 Add Legacy Semi Ring
-  N Nplus Nmult 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
+  N N.add N.mul 1%N 0%N Neq NTheory [ Npos 0%N xO xI 1%positive ].
diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v
index 5845062dd2..5c702c90e6 100644
--- a/plugins/ring/LegacyZArithRing.v
+++ b/plugins/ring/LegacyZArithRing.v
@@ -21,15 +21,15 @@ Definition Zeq (x y:Z) :=
 
 Lemma Zeq_prop : forall x y:Z, Is_true (Zeq x y) -> x = y.
   intros x y H; unfold Zeq in H.
-  apply Zcompare_Eq_eq.
+  apply Z.compare_eq.
   destruct (x ?= y)%Z; [ reflexivity | contradiction | contradiction ].
 Qed.
 
-Definition ZTheory : Ring_Theory Zplus Zmult 1%Z 0%Z Zopp Zeq.
+Definition ZTheory : Ring_Theory Z.add Z.mul 1%Z 0%Z Z.opp Zeq.
   split; intros; eauto with zarith.
   apply Zeq_prop; assumption.
 Qed.
 
 (* NatConstants and NatTheory are defined in Ring_theory.v *)
-Add Legacy Ring Z Zplus Zmult 1%Z 0%Z Zopp Zeq ZTheory
+Add Legacy Ring Z Z.add Z.mul 1%Z 0%Z Z.opp Zeq ZTheory
  [ Zpos Zneg 0%Z xO xI 1%positive ].
diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v
index 1763d70a62..5358941605 100644
--- a/plugins/ring/Ring_abstract.v
+++ b/plugins/ring/Ring_abstract.v
@@ -137,8 +137,7 @@ Hint Resolve (SR_plus_zero_right2 T).
 Hint Resolve (SR_mult_one_right T).
 Hint Resolve (SR_mult_one_right2 T).
 (*Hint Resolve (SR_plus_reg_right T).*)
-Hint Resolve refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+Hint Resolve eq_refl eq_sym eq_trans.
 Hint Immediate T.
 
 Remark iacs_aux_ok :
@@ -446,8 +445,7 @@ Hint Resolve (Th_plus_zero_right2 T).
 Hint Resolve (Th_mult_one_right T).
 Hint Resolve (Th_mult_one_right2 T).
 (*Hint Resolve (Th_plus_reg_right T).*)
-Hint Resolve refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+Hint Resolve eq_refl eq_sym eq_trans.
 Hint Immediate T.
 
 Lemma isacs_aux_ok :
diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v
index c6dff3e006..9755d71e12 100644
--- a/plugins/ring/Ring_normalize.v
+++ b/plugins/ring/Ring_normalize.v
@@ -365,8 +365,7 @@ Hint Resolve (SR_plus_zero_right2 T).
 Hint Resolve (SR_mult_one_right T).
 Hint Resolve (SR_mult_one_right2 T).
 (*Hint Resolve (SR_plus_reg_right T).*)
-Hint Resolve refl_equal sym_equal trans_equal.
-(* Hints Resolve refl_eqT sym_eqT trans_eqT. *)
+Hint Resolve eq_refl eq_sym eq_trans.
 Hint Immediate T.
 
 Lemma varlist_eq_prop : forall x y:varlist, Is_true (varlist_eq x y) -> x = y.
@@ -794,8 +793,7 @@ Hint Resolve (Th_plus_zero_right2 T).
 Hint Resolve (Th_mult_one_right T).
 Hint Resolve (Th_mult_one_right2 T).
 (*Hint Resolve (Th_plus_reg_right T).*)
-Hint Resolve refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+Hint Resolve eq_refl eq_sym eq_trans.
 Hint Immediate T.
 
 (*** Definitions *)
diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v
index ad75a8a4dd..94b36e2467 100644
--- a/plugins/ring/Setoid_ring_normalize.v
+++ b/plugins/ring/Setoid_ring_normalize.v
@@ -387,8 +387,7 @@ Hint Resolve (SSR_plus_zero_right2 S T).
 Hint Resolve (SSR_mult_one_right S T).
 Hint Resolve (SSR_mult_one_right2 S T).
 Hint Resolve (SSR_plus_reg_right S T).
-Hint Resolve refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+Hint Resolve eq_refl eq_sym eq_trans.
 Hint Immediate T.
 
 Lemma varlist_eq_prop : forall x y:varlist, Is_true (varlist_eq x y) -> x = y.
@@ -1052,8 +1051,7 @@ Hint Resolve (STh_plus_zero_right2 S T).
 Hint Resolve (STh_mult_one_right S T).
 Hint Resolve (STh_mult_one_right2 S T).
 Hint Resolve (STh_plus_reg_right S plus_morph T).
-Hint Resolve refl_equal sym_equal trans_equal.
-(*Hints Resolve refl_eqT sym_eqT trans_eqT.*)
+Hint Resolve eq_refl eq_sym eq_trans.
 Hint Immediate T.
 
 
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index ab6ee15735..22d5adb183 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.ml
@@ -451,7 +451,7 @@ let build_polynom gl th lc =
 	  mkLApp(coq_Pplus, [|th.th_a; aux c1; aux c2 |])
       | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
 	  mkLApp(coq_Pmult, [|th.th_a; aux c1; aux c2 |])
-      (* The special case of Zminus *)
+      (* The special case of Z.sub *)
       | App (binop, [|c1; c2|])
 	  when safe_pf_conv_x gl c
             (mkApp (th.th_plus, [|c1; mkApp(unbox th.th_opp, [|c2|])|])) ->
@@ -569,7 +569,7 @@ let build_apolynom gl th lc =
 	  mkLApp(coq_APplus, [| aux c1; aux c2 |])
       | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
 	  mkLApp(coq_APmult, [| aux c1; aux c2 |])
-      (* The special case of Zminus *)
+      (* The special case of Z.sub *)
       | App (binop, [|c1; c2|])
 	  when safe_pf_conv_x gl c
             (mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|]) |])) ->
@@ -630,7 +630,7 @@ let build_setpolynom gl th lc =
 	  mkLApp(coq_SetPplus, [|th.th_a; aux c1; aux c2 |])
       | App (binop, [|c1; c2|]) when safe_pf_conv_x gl binop th.th_mult ->
 	  mkLApp(coq_SetPmult, [|th.th_a; aux c1; aux c2 |])
-      (* The special case of Zminus *)
+      (* The special case of Z.sub *)
       | App (binop, [|c1; c2|])
 	  when safe_pf_conv_x gl c
 	    (mkApp(th.th_plus, [|c1; mkApp(unbox th.th_opp,[|c2|])|])) ->