OrderedType implementation for various numerical datatypes + min/max structures

 - A richer OrderedTypeFull interface : OrderedType + predicate "le"
 - Implementations {Nat,N,P,Z,Q}OrderedType.v, also providing "order" tactics
 - By the way: as suggested by S. Lescuyer, specification of compare is
   now inductive
 - GenericMinMax: axiomatisation + properties of min and max out of
    OrderedTypeFull structures.
 - MinMax.v, {Z,P,N,Q}minmax.v are specialization of GenericMinMax,
    with also some domain-specific results, and compatibility layer
    with already existing results.
 - Some ML code of plugins had to be adapted, otherwise wrong "eq",
   "lt" or simimlar constants were found by functions like coq_constant.
 - Beware of the aliasing problems: for instance eq:=@eq t instead of
   eq:=@eq M.t in Make_UDT made (r)omega stopped working (Z_as_OT.t
   instead of Z in statement of Zmax_spec).
 - Some Morphism declaration are now ambiguous: switch to new syntax
   anyway.
 - Misc adaptations of FSets/MSets
 - Classes/RelationPairs.v: from two relations over A and B, we
   inspect relations over A*B and their properties in terms of classes.

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

6 files changed, 58 insertions, 52 deletions

diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 19a884323..53359e31d 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -128,7 +128,7 @@ let def_of_const t =
 
 let coq_constant s =
   Coqlib.gen_constant_in_modules "RecursiveDefinition"
-    (Coqlib.init_modules @ Coqlib.arith_modules) s;;
+    Coqlib.init_modules s;;
 
 let constant sl s =
   constr_of_global
@@ -142,7 +142,7 @@ let find_reference sl s =
 	       (id_of_string s)));;
 
 let eq = lazy(coq_constant "eq")
-let refl_equal = lazy(coq_constant "refl_equal")
+let refl_equal = lazy(coq_constant "eq_refl")
 
 (*****************************************************************)
 (* Copy of the standart save mechanism but without the much too  *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 92438db39..5499425df 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -236,6 +236,10 @@ let coq_constant s =
   Coqlib.gen_constant_in_modules "RecursiveDefinition"
     (Coqlib.init_modules @ Coqlib.arith_modules) s;;
 
+let coq_base_constant s =
+  Coqlib.gen_constant_in_modules "RecursiveDefinition"
+    (Coqlib.init_modules @ [["Coq";"Arith";"Le"];["Coq";"Arith";"Lt"]]) s;;
+
 let constant sl s =
   constr_of_global
     (locate (make_qualid(Names.make_dirpath
@@ -250,23 +254,23 @@ let find_reference sl s =
 let delayed_force f = f ()
 
 let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
-let le_lt_n_Sm = function () -> (coq_constant "le_lt_n_Sm")
-
-let le_trans = function () -> (coq_constant "le_trans")
-let le_lt_trans = function () -> (coq_constant "le_lt_trans")
-let lt_S_n = function () -> (coq_constant "lt_S_n")
-let le_n = function () -> (coq_constant "le_n")
-let refl_equal = function () -> (coq_constant "refl_equal")
-let eq = function () -> (coq_constant "eq")
-let ex = function () -> (coq_constant "ex")
+let le_lt_n_Sm = function () -> (coq_base_constant "le_lt_n_Sm")
+
+let le_trans = function () -> (coq_base_constant "le_trans")
+let le_lt_trans = function () -> (coq_base_constant "le_lt_trans")
+let lt_S_n = function () -> (coq_base_constant "lt_S_n")
+let le_n = function () -> (coq_base_constant "le_n")
+let refl_equal = function () -> (coq_base_constant "eq_refl")
+let eq = function () -> (coq_base_constant "eq")
+let ex = function () -> (coq_base_constant "ex")
 let coq_sig_ref = function () -> (find_reference ["Coq";"Init";"Specif"] "sig")
-let coq_sig = function () -> (coq_constant "sig")
-let coq_O = function () -> (coq_constant "O")
-let coq_S = function () -> (coq_constant "S")
+let coq_sig = function () -> (coq_base_constant "sig")
+let coq_O = function () -> (coq_base_constant "O")
+let coq_S = function () -> (coq_base_constant "S")
 
 let gt_antirefl = function () -> (coq_constant "gt_irrefl")
-let lt_n_O = function () -> (coq_constant "lt_n_O")
-let lt_n_Sn = function () -> (coq_constant "lt_n_Sn")
+let lt_n_O = function () -> (coq_base_constant "lt_n_O")
+let lt_n_Sn = function () -> (coq_base_constant "lt_n_Sn")
 
 let f_equal = function () -> (coq_constant "f_equal")
 let well_founded_induction = function () -> (coq_constant "well_founded_induction")
@@ -284,8 +288,8 @@ let coq_conj = function () -> find_reference ["Coq";"Init";"Logic"] "conj"
 
 (* These are specific to experiments in nat with lt as well_founded_relation, *)
 (*    but this should be made more general. *)
-let nat = function () -> (coq_constant "nat")
-let lt = function () -> (coq_constant "lt")
+let nat = function () -> (coq_base_constant "nat")
+let lt = function () -> (coq_base_constant "lt")
 
 (* This is simply an implementation of the case_eq tactic.  this code
   should be replaced with the tactic defined in Ltac in Init/Tactics.v *)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index cc667aa05..10cde3c56 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -136,22 +136,23 @@ struct
      ["Coq";"Reals" ; "Rpow_def"];
      ["LRing_normalise"]]
 
+ let init_constant = gen_constant_in_modules "ZMicromega" init_modules
  let constant = gen_constant_in_modules "ZMicromega" coq_modules
 
- let coq_and = lazy (constant "and")
- let coq_or = lazy (constant "or")
- let coq_not = lazy (constant "not")
- let coq_iff = lazy (constant "iff")
- let coq_True = lazy (constant "True")
- let coq_False = lazy (constant "False")
+ let coq_and = lazy (init_constant "and")
+ let coq_or = lazy (init_constant "or")
+ let coq_not = lazy (init_constant "not")
+ let coq_iff = lazy (init_constant "iff")
+ let coq_True = lazy (init_constant "True")
+ let coq_False = lazy (init_constant "False")
 
  let coq_cons = lazy (constant "cons")
  let coq_nil = lazy (constant "nil")
  let coq_list = lazy (constant "list")
 
- let coq_O = lazy (constant "O")
- let coq_S = lazy (constant "S")
- let coq_nat = lazy (constant "nat")
+ let coq_O = lazy (init_constant "O")
+ let coq_S = lazy (init_constant "S")
+ let coq_nat = lazy (init_constant "nat")
 
  let coq_NO = lazy
   (gen_constant_in_modules "N" [ ["Coq";"NArith";"BinNat" ]]  "N0")
@@ -205,7 +206,7 @@ struct
  let coq_Zge = lazy (constant "Zge")
  let coq_Zle = lazy (constant "Zle")
  let coq_Zlt = lazy (constant "Zlt")
- let coq_Eq  = lazy (constant "eq")
+ let coq_Eq  = lazy (init_constant "eq")
 
  let coq_Zplus = lazy (constant "Zplus")
  let coq_Zminus = lazy (constant "Zminus")
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index e037ee8bf..02d70da74 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -162,12 +162,11 @@ let hide_constr,find_constr,clear_tables,dump_tables =
 open Coqlib
 
 let logic_dir = ["Coq";"Logic";"Decidable"]
-let init_arith_modules = init_modules @ arith_modules
 let coq_modules =
-  init_arith_modules @ [logic_dir] @ zarith_base_modules
+  init_modules @arith_modules @ [logic_dir] @ zarith_base_modules
     @ [["Coq"; "omega"; "OmegaLemmas"]]
 
-let init_arith_constant = gen_constant_in_modules "Omega" init_arith_modules
+let init_constant = gen_constant_in_modules "Omega" init_modules
 let constant = gen_constant_in_modules "Omega" coq_modules
 
 (* Zarith *)
@@ -268,17 +267,17 @@ let coq_Zge = lazy (constant "Zge")
 let coq_Zlt = lazy (constant "Zlt")
 
 (* Peano/Datatypes *)
-let coq_le = lazy (init_arith_constant "le")
-let coq_lt = lazy (init_arith_constant "lt")
-let coq_ge = lazy (init_arith_constant "ge")
-let coq_gt = lazy (init_arith_constant "gt")
-let coq_minus = lazy (init_arith_constant "minus")
-let coq_plus = lazy (init_arith_constant "plus")
-let coq_mult = lazy (init_arith_constant "mult")
-let coq_pred = lazy (init_arith_constant "pred")
-let coq_nat = lazy (init_arith_constant "nat")
-let coq_S = lazy (init_arith_constant "S")
-let coq_O = lazy (init_arith_constant "O")
+let coq_le = lazy (init_constant "le")
+let coq_lt = lazy (init_constant "lt")
+let coq_ge = lazy (init_constant "ge")
+let coq_gt = lazy (init_constant "gt")
+let coq_minus = lazy (init_constant "minus")
+let coq_plus = lazy (init_constant "plus")
+let coq_mult = lazy (init_constant "mult")
+let coq_pred = lazy (init_constant "pred")
+let coq_nat = lazy (init_constant "nat")
+let coq_S = lazy (init_constant "S")
+let coq_O = lazy (init_constant "O")
 
 (* Compare_dec/Peano_dec/Minus *)
 let coq_pred_of_minus = lazy (constant "pred_of_minus")
diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 2978d699e..796b3c7d1 100644
--- a/plugins/romega/const_omega.ml
+++ b/plugins/romega/const_omega.ml
@@ -56,17 +56,19 @@ let coq_modules =
     @ [module_refl_path]
     @ [module_refl_path@["ZOmega"]]
 
+
+let init_constant = Coqlib.gen_constant_in_modules "Omega" Coqlib.init_modules
 let constant = Coqlib.gen_constant_in_modules "Omega" coq_modules
 
 (* Logic *)
-let coq_eq = lazy(constant  "eq")
-let coq_refl_equal = lazy(constant  "refl_equal")
-let coq_and = lazy(constant "and")
-let coq_not = lazy(constant "not")
-let coq_or = lazy(constant "or")
-let coq_True = lazy(constant "True")
-let coq_False = lazy(constant "False")
-let coq_I = lazy(constant "I")
+let coq_eq = lazy(init_constant  "eq")
+let coq_refl_equal = lazy(init_constant  "eq_refl")
+let coq_and = lazy(init_constant "and")
+let coq_not = lazy(init_constant "not")
+let coq_or = lazy(init_constant "or")
+let coq_True = lazy(init_constant "True")
+let coq_False = lazy(init_constant "False")
+let coq_I = lazy(init_constant "I")
 
 (* ReflOmegaCore/ZOmega *)
 
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 205bef6d5..9617d4091 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -439,11 +439,11 @@ Fixpoint PExpr_eq (e1 e2 : PExpr C) {struct e1} : bool :=
   | _, _ => false
  end.
 
-Add Morphism (pow_pos rmul) : pow_morph.
+Add Morphism (pow_pos rmul) with signature req ==> eq ==> req as pow_morph.
 intros x y H p;induction p as [p IH| p IH|];simpl;auto;ring[IH].
 Qed.
 
-Add Morphism (pow_N rI rmul) with signature req ==> (@eq N) ==> req as pow_N_morph.
+Add Morphism (pow_N rI rmul) with signature req ==> eq ==> req as pow_N_morph.
 intros x y H [|p];simpl;auto. apply pow_morph;trivial.
 Qed.
 (*