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

1 files changed, 10 insertions, 8 deletions

diff --git a/plugins/romega/const_omega.ml b/plugins/romega/const_omega.ml
index 2978d699e1..796b3c7d1d 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 *)