diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-29 14:31:32 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-04-29 14:31:32 +0000 |
| commit | 3eafff483153eac36c99b025a38bc1735f7c4a8b (patch) | |
| tree | 41f06a36553307b44df56c06a7c4ca7e67d7c2f1 /Makefile | |
| parent | c03302b1783ddd7a78902689b57787bed67c1f88 (diff) | |
suite de l'ajout des FSets/FMaps dans les theories standards
-> OrderedTypeEx: des exemples de OrderedType
-> OrderedTypeAlt: une definition alternative de OrderedType
-> FSetAVL et FMapAVL: realisation a coup d'AVL
-> FMapPositive: realisation a coup d'arbre binaire
(selon les chiffres binaires de la cle)
-> FMapIntMap : realisation en utilisant IntMap
-> FSetToFiniteSet: un ensemble de FSet est un ensemble de Ensemble.v
FSetAVL et FMapAVL prenent 30 secondes chacuns sur ma machine:
on peut ne pas les compiler en passant l'option "-fsets no" a
configure, de facon similaire a "-reals no"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8773 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 19 |
1 files changed, 16 insertions, 3 deletions
@@ -863,8 +863,9 @@ SETSVO=\ theories/Sets/Multiset.vo theories/Sets/Relations_3_facts.vo \ theories/Sets/Partial_Order.vo theories/Sets/Uniset.vo -FSETSVO=\ +FSETSBASEVO=\ theories/FSets/DecidableType.vo theories/FSets/OrderedType.vo \ + theories/FSets/OrderedTypeEx.vo theories/FSets/OrderedTypeAlt.vo \ theories/FSets/FSetInterface.vo theories/FSets/FSetList.vo \ theories/FSets/FSetBridge.vo theories/FSets/FSetFacts.vo \ theories/FSets/FSetProperties.vo theories/FSets/FSetEqProperties.vo \ @@ -874,7 +875,18 @@ FSETSVO=\ theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo \ theories/FSets/FMaps.vo \ theories/FSets/FMapWeakInterface.vo theories/FSets/FMapWeakList.vo \ - theories/FSets/FMapWeak.vo + theories/FSets/FMapWeak.vo theories/FSets/FMapPositive.vo \ + theories/FSets/FMapIntMap.vo theories/FSets/FSetToFiniteSet.vo \ + theories/FSets/Int.vo \ + +FSETS_basic= + +FSETS_all=\ + theories/FSets/FMapAVL.vo theories/FSets/FSetAVL.vo \ + +FSETSVO=$(FSETSBASEVO) $(FSETS_$(FSETS)) + +ALLFSETS=$(FSETSBASEVO) $(FSETS_all) INTMAPVO=\ theories/IntMap/Adalloc.vo theories/IntMap/Mapcanon.vo \ @@ -963,6 +975,7 @@ lists: $(LISTSVO) strings: $(STRINGSVO) sets: $(SETSVO) fsets: $(FSETSVO) +allfsets: $(ALLFSETS) intmap: $(INTMAPVO) relations: $(RELATIONSVO) wellfounded: $(WELLFOUNDEDVO) @@ -1610,7 +1623,7 @@ alldepend: depend dependcoq dependcoq:: beforedepend $(COQDEP) -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) \ - $(ALLREALS:.vo=.v) $(ALLVO:.vo=.v) > .depend.coq + $(ALLFSETS:.vo=.v) $(ALLREALS:.vo=.v) $(ALLVO:.vo=.v) > .depend.coq # Build dependencies ignoring failures in building ml files from ml4 files # This is useful to rebuild dependencies when they are strongly corrupted: |