aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/ZArith/ZArith_base.v
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-03 08:24:06 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2009-11-03 08:24:06 +0000
commit4f0ad99adb04e7f2888e75f2a10e8c916dde179b (patch)
tree4b52d7436fe06f4b2babfd5bfed84762440e7de7 /theories/ZArith/ZArith_base.v
parent4e68924f48d3f6d5ffdf1cd394b590b5a6e15ea1 (diff)
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
Diffstat (limited to 'theories/ZArith/ZArith_base.v')
-rw-r--r--theories/ZArith/ZArith_base.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/ZArith_base.v b/theories/ZArith/ZArith_base.v
index 956221cb3..cd866c375 100644
--- a/theories/ZArith/ZArith_base.v
+++ b/theories/ZArith/ZArith_base.v
@@ -18,9 +18,9 @@ Require Export BinInt.
Require Export Zcompare.
Require Export Zorder.
Require Export Zeven.
+Require Export Zminmax.
Require Export Zmin.
Require Export Zmax.
-Require Export Zminmax.
Require Export Zabs.
Require Export Znat.
Require Export auxiliary.