diff options
| author | letouzey | 2009-11-10 11:19:25 +0000 |
|---|---|---|
| committer | letouzey | 2009-11-10 11:19:25 +0000 |
| commit | e8b2255678a7fa1c140c4a50dca26cc94ac1a6e0 (patch) | |
| tree | e1dcc1538e1ce09783a7d4fccc94c6aeb75b29e0 /Makefile.common | |
| parent | 424b20ed34966506cef31abf85e3e3911138f0fc (diff) | |
Simplification of Numbers, mainly thanks to Include
- No more nesting of Module and Module Type, we rather use Include.
- Instead of in-name-qualification like NZeq, we use uniform
short names + modular qualification like N.eq when necessary.
- Many simplification of proofs, by some autorewrite for instance
- In NZOrder, we instantiate an "order" tactic.
- Some requirements in NZAxioms were superfluous: compatibility
of le, min and max could be derived from the rest.
- NMul removed, since it was containing only an ad-hoc result for
ZNatPairs, that we've inlined in the proof of mul_wd there.
- Zdomain removed (was already not compiled), idea of a module
with eq and eqb reused in DecidableType.BooleanEqualityType.
- ZBinDefs don't contain any definition now, migrate it to ZBinary.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12489 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/Makefile.common b/Makefile.common index ae684974a2..64036168e6 100644 --- a/Makefile.common +++ b/Makefile.common @@ -459,18 +459,18 @@ CYCLICVO:=$(CYCLICABSTRACTVO) $(CYCLICINT31VO) $(CYCLICDOUBLECYCLICVO) \ NATINTVO:=$(addprefix theories/Numbers/NatInt/, \ NZAxioms.vo NZBase.vo NZAdd.vo NZMul.vo \ - NZOrder.vo NZAddOrder.vo NZMulOrder.vo ) + NZOrder.vo NZAddOrder.vo NZMulOrder.vo NZProperties.vo) NATURALABSTRACTVO:=$(addprefix theories/Numbers/Natural/Abstract/, \ - NAxioms.vo NBase.vo NAdd.vo NMul.vo \ + NAxioms.vo NBase.vo NAdd.vo \ NOrder.vo NAddOrder.vo NMulOrder.vo NSub.vo \ - NIso.vo NStrongRec.vo NDefOps.vo) + NProperties.vo NIso.vo NStrongRec.vo NDefOps.vo) NATURALPEANOVO:=$(addprefix theories/Numbers/Natural/Peano/, \ NPeano.vo ) NATURALBINARYVO:=$(addprefix theories/Numbers/Natural/Binary/, \ - NBinDefs.vo NBinary.vo ) + NBinary.vo ) NATURALSPECVIAZVO:=$(addprefix theories/Numbers/Natural/SpecViaZ/, \ NSig.vo NSigNAxioms.vo ) @@ -483,7 +483,7 @@ NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO) \ INTEGERABSTRACTVO:=$(addprefix theories/Numbers/Integer/Abstract/, \ ZAxioms.vo ZBase.vo ZAdd.vo ZMul.vo \ - ZLt.vo ZAddOrder.vo ZMulOrder.vo ) + ZLt.vo ZAddOrder.vo ZMulOrder.vo ZProperties.vo) INTEGERBINARYVO:=$(addprefix theories/Numbers/Integer/Binary/, \ ZBinary.vo ) |