diff options
| author | letouzey | 2009-11-03 08:24:06 +0000 |
|---|---|---|
| committer | letouzey | 2009-11-03 08:24:06 +0000 |
| commit | 4f0ad99adb04e7f2888e75f2a10e8c916dde179b (patch) | |
| tree | 4b52d7436fe06f4b2babfd5bfed84762440e7de7 /Makefile.common | |
| parent | 4e68924f48d3f6d5ffdf1cd394b590b5a6e15ea1 (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 'Makefile.common')
| -rw-r--r-- | Makefile.common | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/Makefile.common b/Makefile.common index 06e5f3b4bb..b680dc1397 100644 --- a/Makefile.common +++ b/Makefile.common @@ -316,8 +316,9 @@ STRUCTURESVO:=$(addprefix theories/Structures/, \ OrderTac.vo \ DecidableType.vo DecidableTypeEx.vo \ OrderedType.vo OrderedTypeEx.vo OrderedTypeAlt.vo \ - DecidableType2.vo DecidableType2Ex.vo \ - OrderedType2.vo OrderedType2Ex.vo OrderedType2Alt.vo ) + DecidableType2.vo DecidableType2Ex.vo DecidableType2Facts.vo \ + OrderedType2.vo OrderedType2Ex.vo OrderedType2Alt.vo \ + OrderedType2Facts.vo OrderedType2Lists.vo GenericMinMax.vo ) ARITHVO:=$(addprefix theories/Arith/, \ Arith.vo Gt.vo Between.vo Le.vo \ @@ -325,7 +326,7 @@ ARITHVO:=$(addprefix theories/Arith/, \ Div2.vo Minus.vo Mult.vo Even.vo \ EqNat.vo Peano_dec.vo Euclid.vo Plus.vo \ Wf_nat.vo Max.vo Bool_nat.vo Factorial.vo \ - Arith_base.vo ) + Arith_base.vo MinMax.vo NatOrderedType.vo ) SORTINGVO:=$(addprefix theories/Sorting/, \ Heap.vo Permutation.vo Sorting.vo PermutSetoid.vo \ @@ -337,7 +338,8 @@ BOOLVO:=$(addprefix theories/Bool/, \ NARITHVO:=$(addprefix theories/NArith/, \ BinPos.vo Pnat.vo BinNat.vo NArith.vo \ - Nnat.vo Ndigits.vo Ndec.vo Ndist.vo ) + Nnat.vo Ndigits.vo Ndec.vo Ndist.vo \ + POrderedType.vo Pminmax.vo NOrderedType.vo Nminmax.vo ) ZARITHVO:=$(addprefix theories/ZArith/, \ BinInt.vo Wf_Z.vo ZArith.vo ZArith_dec.vo \ @@ -347,7 +349,7 @@ ZARITHVO:=$(addprefix theories/ZArith/, \ Zpower.vo Zcomplements.vo Zdiv.vo Zsqrt.vo \ Zwf.vo ZArith_base.vo Zbool.vo Zbinary.vo \ Znumtheory.vo Int.vo Zpow_def.vo Zpow_facts.vo \ - ZOdiv_def.vo ZOdiv.vo Zgcd_alt.vo ) + ZOdiv_def.vo ZOdiv.vo Zgcd_alt.vo ZOrderedType.vo ) QARITHVO:=$(addprefix theories/QArith/, \ QArith_base.vo Qreduction.vo Qring.vo Qreals.vo \ @@ -517,7 +519,8 @@ UNICODEVO:=$(addprefix theories/Unicode/, \ CLASSESVO:=$(addprefix theories/Classes/, \ Init.vo RelationClasses.vo Morphisms.vo Morphisms_Prop.vo \ Morphisms_Relations.vo Functions.vo Equivalence.vo SetoidTactics.vo \ - SetoidClass.vo SetoidAxioms.vo EquivDec.vo SetoidDec.vo ) + SetoidClass.vo SetoidAxioms.vo EquivDec.vo SetoidDec.vo \ + RelationPairs.vo ) PROGRAMVO:=$(addprefix theories/Program/, \ Tactics.vo Equality.vo Subset.vo Utils.vo \ |