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, 13 insertions, 14 deletions

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")