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, 11 insertions, 10 deletions

diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index cc667aa05c..10cde3c56b 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")