diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-01 13:28:59 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-06-01 13:28:59 +0000 |
| commit | f785876d6e2aba5ee2340499763dc9a52b36130b (patch) | |
| tree | 89c18f96068afe494e63906693093e92f1efb484 /Makefile.common | |
| parent | 98231b971df2323c16fef638c0b3fd2ba8eab07f (diff) | |
Enhance the BigN and BigZ infrastructure:
* Isolate and put forward the interfaces NSig and ZSig that describe
what should contain structures of natural numbers and integers (specs
are done by translation to ZArith).
* Functors NSigNAxioms and ZSigZAxioms proving that these NSig and
ZSig implements the fully-abstract NAxioms and ZAxioms module types.
* BigN and BigZ now contains more notations, plus an export of all
abstract results proved by Evgeny instantiated thanks to NSigNAxioms
and ZSigZAxioms. In addition, BigN and BigZ are declared as
(semi/full)-rings.
* as a consequence, some incompatibities have to be fixed in BigQ:
- take care of some name masking (via Import, Open Scope ...)
- some additionnal constants like BigN.lt to deal with
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11027 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 13 |
1 files changed, 10 insertions, 3 deletions
diff --git a/Makefile.common b/Makefile.common index c968b41b8..0053dafdc 100644 --- a/Makefile.common +++ b/Makefile.common @@ -685,10 +685,14 @@ NATURALPEANOVO:=$(addprefix theories/Numbers/Natural/Peano/, \ NATURALBINARYVO:=$(addprefix theories/Numbers/Natural/Binary/, \ NBinDefs.vo NBinary.vo ) +NATURALSPECVIAZVO:=$(addprefix theories/Numbers/Natural/SpecViaZ/, \ + NSig.vo NSigNAxioms.vo ) + NATURALBIGNVO:=$(addprefix theories/Numbers/Natural/BigN/, \ - Nbasic.vo NMake.vo BigN.vo NBigN.vo ) + Nbasic.vo NMake.vo BigN.vo ) -NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO) $(NATURALBIGNVO) +NATURALVO:=$(NATURALABSTRACTVO) $(NATURALPEANOVO) $(NATURALBINARYVO) \ + $(NATURALSPECVIAZVO) $(NATURALBIGNVO) INTEGERABSTRACTVO:=$(addprefix theories/Numbers/Integer/Abstract/, \ ZAxioms.vo ZBase.vo ZPlus.vo ZTimes.vo \ @@ -700,11 +704,14 @@ INTEGERBINARYVO:=$(addprefix theories/Numbers/Integer/Binary/, \ INTEGERNATPAIRSVO:=$(addprefix theories/Numbers/Integer/NatPairs/, \ ZNatPairs.vo ) +INTEGERSPECVIAZVO:=$(addprefix theories/Numbers/Integer/SpecViaZ/, \ + ZSig.vo ZSigZAxioms.vo ) + INTEGERBIGZVO:=$(addprefix theories/Numbers/Integer/BigZ/, \ ZMake.vo BigZ.vo ) INTEGERVO:=$(INTEGERABSTRACTVO) $(INTEGERBINARYVO) $(INTEGERNATPAIRSVO) \ - $(INTEGERBIGZVO) + $(INTEGERSPECVIAZVO) $(INTEGERBIGZVO) RATIONALBIGQVO:=$(addprefix theories/Numbers/Rational/BigQ/, \ QMake_base.vo QpMake.vo QvMake.vo Q0Make.vo \ |