From 3eafff483153eac36c99b025a38bc1735f7c4a8b Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 29 Apr 2006 14:31:32 +0000
Subject: 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
---
 Makefile | 19 ++++++++++++++++---
 1 file changed, 16 insertions(+), 3 deletions(-)

(limited to 'Makefile')

diff --git a/Makefile b/Makefile
index 2ce9d466b..a91a7366d 100644
--- a/Makefile
+++ b/Makefile
@@ -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:
-- 
cgit v1.2.3