ZArith + other : favor the use of modern names instead of compat notations

 - For instance, refl_equal --> eq_refl
 - Npos, Zpos, Zneg now admit more uniform qualified aliases
   N.pos, Z.pos, Z.neg.
 - A new module BinInt.Pos2Z with results about injections from
   positive to Z
 - A result about Z.pow pushed in the generic layer
 - Zmult_le_compat_{r,l} --> Z.mul_le_mono_nonneg_{r,l}
 - Using tactic Z.le_elim instead of Zle_lt_or_eq
 - Some cleanup in ring, field, micromega
   (use of "Equivalence", "Proper" ...)
 - Some adaptions in QArith (for instance changed Qpower.Qpower_decomp)
 - In ZMake and ZMake, functor parameters are now named NN and ZZ
   instead of N and Z for avoiding confusions

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15515 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 23 insertions, 30 deletions

diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v
index 5dcd6d840..a69cf0957 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 5845062dd..5c702c90e 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 1763d70a6..535894160 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 c6dff3e00..9755d71e1 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 ad75a8a4d..94b36e246 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 ab6ee1573..22d5adb18 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|])|])) ->