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

1 files changed, 30 insertions, 27 deletions

diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 2a98cae53..9fa18e7dc 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -173,6 +173,9 @@ let init_constant = gen_constant_in_modules "Omega" init_modules
 let constant = gen_constant_in_modules "Omega" coq_modules
 
 let z_constant = gen_constant_in_modules "Omega" [["Coq";"ZArith"]]
+let zbase_constant =
+  gen_constant_in_modules "Omega" [["Coq";"ZArith";"BinInt"]]
+
 
 (* Zarith *)
 let coq_xH = lazy (constant "xH")
@@ -184,20 +187,20 @@ let coq_Zneg = lazy (constant "Zneg")
 let coq_Z = lazy (constant "Z")
 let coq_comparison = lazy (constant "comparison")
 let coq_Gt = lazy (constant "Gt")
-let coq_Zplus = lazy (constant "Zplus")
-let coq_Zmult = lazy (constant "Zmult")
-let coq_Zopp = lazy (constant "Zopp")
-let coq_Zminus = lazy (constant "Zminus")
-let coq_Zsucc = lazy (constant "Zsucc")
-let coq_Zpred = lazy (constant "Zpred")
-let coq_Zgt = lazy (constant "Zgt")
-let coq_Zle = lazy (constant "Zle")
-let coq_Z_of_nat = lazy (constant "Z_of_nat")
-let coq_inj_plus = lazy (constant "inj_plus")
-let coq_inj_mult = lazy (constant "inj_mult")
-let coq_inj_minus1 = lazy (constant "inj_minus1")
+let coq_Zplus = lazy (zbase_constant "Z.add")
+let coq_Zmult = lazy (zbase_constant "Z.mul")
+let coq_Zopp = lazy (zbase_constant "Z.opp")
+let coq_Zminus = lazy (zbase_constant "Z.sub")
+let coq_Zsucc = lazy (zbase_constant "Z.succ")
+let coq_Zpred = lazy (zbase_constant "Z.pred")
+let coq_Zgt = lazy (zbase_constant "Z.gt")
+let coq_Zle = lazy (zbase_constant "Z.le")
+let coq_Z_of_nat = lazy (zbase_constant "Z.of_nat")
+let coq_inj_plus = lazy (z_constant "Nat2Z.inj_add")
+let coq_inj_mult = lazy (z_constant "Nat2Z.inj_mul")
+let coq_inj_minus1 = lazy (z_constant "Nat2Z.inj_sub")
 let coq_inj_minus2 = lazy (constant "inj_minus2")
-let coq_inj_S = lazy (z_constant "inj_S")
+let coq_inj_S = lazy (z_constant "Nat2Z.inj_succ")
 let coq_inj_le = lazy (z_constant "Znat.inj_le")
 let coq_inj_lt = lazy (z_constant "Znat.inj_lt")
 let coq_inj_ge = lazy (z_constant "Znat.inj_ge")
@@ -253,10 +256,10 @@ let coq_Zle_left = lazy (constant "Zle_left")
 let coq_new_var = lazy (constant "new_var")
 let coq_intro_Z = lazy (constant "intro_Z")
 
-let coq_dec_eq = lazy (constant "dec_eq")
+let coq_dec_eq = lazy (zbase_constant "Z.eq_decidable")
 let coq_dec_Zne = lazy (constant "dec_Zne")
-let coq_dec_Zle = lazy (constant "dec_Zle")
-let coq_dec_Zlt = lazy (constant "dec_Zlt")
+let coq_dec_Zle = lazy (zbase_constant "Z.le_decidable")
+let coq_dec_Zlt = lazy (zbase_constant "Z.lt_decidable")
 let coq_dec_Zgt = lazy (constant "dec_Zgt")
 let coq_dec_Zge = lazy (constant "dec_Zge")
 
@@ -268,10 +271,10 @@ let coq_Znot_ge_lt = lazy (constant "Znot_ge_lt")
 let coq_Znot_gt_le = lazy (constant "Znot_gt_le")
 let coq_neq = lazy (constant "neq")
 let coq_Zne = lazy (constant "Zne")
-let coq_Zle = lazy (constant "Zle")
-let coq_Zgt = lazy (constant "Zgt")
-let coq_Zge = lazy (constant "Zge")
-let coq_Zlt = lazy (constant "Zlt")
+let coq_Zle = lazy (zbase_constant "Z.le")
+let coq_Zgt = lazy (zbase_constant "Z.gt")
+let coq_Zge = lazy (zbase_constant "Z.ge")
+let coq_Zlt = lazy (zbase_constant "Z.lt")
 
 (* Peano/Datatypes *)
 let coq_le = lazy (init_constant "le")
@@ -329,13 +332,13 @@ let evaluable_ref_of_constr s c = match kind_of_term (Lazy.force c) with
       EvalConstRef kn
   | _ -> anomaly ("Coq_omega: "^s^" is not an evaluable constant")
 
-let sp_Zsucc =     lazy (evaluable_ref_of_constr "Zsucc" coq_Zsucc)
-let sp_Zpred =     lazy (evaluable_ref_of_constr "Zpred" coq_Zpred)
-let sp_Zminus = lazy (evaluable_ref_of_constr "Zminus" coq_Zminus)
-let sp_Zle = lazy (evaluable_ref_of_constr "Zle" coq_Zle)
-let sp_Zgt = lazy (evaluable_ref_of_constr "Zgt" coq_Zgt)
-let sp_Zge = lazy (evaluable_ref_of_constr "Zge" coq_Zge)
-let sp_Zlt = lazy (evaluable_ref_of_constr "Zlt" coq_Zlt)
+let sp_Zsucc =     lazy (evaluable_ref_of_constr "Z.succ" coq_Zsucc)
+let sp_Zpred =     lazy (evaluable_ref_of_constr "Z.pred" coq_Zpred)
+let sp_Zminus = lazy (evaluable_ref_of_constr "Z.sub" coq_Zminus)
+let sp_Zle = lazy (evaluable_ref_of_constr "Z.le" coq_Zle)
+let sp_Zgt = lazy (evaluable_ref_of_constr "Z.gt" coq_Zgt)
+let sp_Zge = lazy (evaluable_ref_of_constr "Z.ge" coq_Zge)
+let sp_Zlt = lazy (evaluable_ref_of_constr "Z.lt" coq_Zlt)
 let sp_not = lazy (evaluable_ref_of_constr "not" (lazy (build_coq_not ())))
 
 let mk_var v = mkVar (id_of_string v)