diff options
| author | letouzey | 2008-03-19 20:56:43 +0000 |
|---|---|---|
| committer | letouzey | 2008-03-19 20:56:43 +0000 |
| commit | 509cd11ac957c0ff97cbe9a0cd50852c74095e36 (patch) | |
| tree | aeadbbc55f35b9c572a4f76084bb5ec7a5c9e401 /Makefile.common | |
| parent | 0157aadd967fcba870fb9bf74ea2af7671105efc (diff) | |
migration of the old IntMap library from StdLib to a user contrib (Cachan/IntMap)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10699 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
| -rw-r--r-- | Makefile.common | 21 |
1 files changed, 6 insertions, 15 deletions
diff --git a/Makefile.common b/Makefile.common index 36cf5a80c3..3c606c739c 100644 --- a/Makefile.common +++ b/Makefile.common @@ -610,28 +610,19 @@ FSETSBASEVO:=\ theories/FSets/FMapInterface.vo theories/FSets/FMapList.vo \ theories/FSets/FMaps.vo theories/FSets/FMapFacts.vo \ theories/FSets/FMapWeakList.vo theories/FSets/FMapPositive.vo \ - theories/FSets/FMapIntMap.vo theories/FSets/FSetToFiniteSet.vo \ - theories/FSets/FSetDecide.vo + theories/FSets/FSetToFiniteSet.vo theories/FSets/FSetDecide.vo \ + theories/FSets/FSetAVL.vo FSETS_basic:= FSETS_all:=\ - theories/FSets/FSetAVL.vo theories/FSets/FSetFullAVL.vo \ - theories/FSets/FMapAVL.vo + theories/FSets/FSetFullAVL.vo \ + theories/FSets/FMapAVL.vo FSETSVO:=$(FSETSBASEVO) $(FSETS_$(FSETS)) ALLFSETS:=$(FSETSBASEVO) $(FSETS_all) -INTMAPVO:=\ - theories/IntMap/Adalloc.vo theories/IntMap/Mapcanon.vo \ - theories/IntMap/Mapfold.vo \ - theories/IntMap/Mapcard.vo theories/IntMap/Mapc.vo \ - theories/IntMap/Allmaps.vo theories/IntMap/Mapiter.vo \ - theories/IntMap/Fset.vo theories/IntMap/Maplists.vo \ - theories/IntMap/Lsort.vo theories/IntMap/Mapsubset.vo \ - theories/IntMap/Mapaxioms.vo theories/IntMap/Map.vo \ - RELATIONSVO:=\ theories/Relations/Newman.vo \ theories/Relations/Operators_Properties.vo \ @@ -754,7 +745,7 @@ CLASSESVO:= theories/Classes/Init.vo theories/Classes/RelationClasses.vo theorie THEORIESVO:=\ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(NARITHVO) $(ZARITHVO) \ - $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(INTMAPVO) \ + $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) \ $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO) $(SORTINGVO) $(QARITHVO) \ $(INTSVO) $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) @@ -873,7 +864,7 @@ STAGE2_TARGETS:=$(COQBINARIES) lib kernel byterun library proofs tactics \ pcoq-binaries $(COQINTERFACE) coqbinaries pcoq $(TOOLS) tools \ printers $(MINICOQ) debug VO_TARGETS:=logic arith bool narith zarith qarith lists strings sets \ - fsets allfsets intmap relations wellfounded ints reals allreals \ + fsets allfsets relations wellfounded ints reals allreals \ setoids sorting natural integer rational numbers noreal \ omega ring setoid_ring dp xml extraction field fourier jprover \ funind cc programs subtac rtauto |