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

1 files changed, 25 insertions, 0 deletions

diff --git a/configure b/configure
index e827b4ef9..5b031ccac 100755
--- a/configure
+++ b/configure
@@ -36,6 +36,8 @@ mandir_spec=no
 emacslib_spec=no
 emacs_spec=no
 coqdocdir_spec=no
+fsets_opt=no
+fsets=all
 reals_opt=no
 reals=all
 arch_spec=no
@@ -69,6 +71,8 @@ while : ; do
 		    emacslib=$COQTOP/tools/emacs
 		    coqdocdir_spec=yes
 		    coqdocdir=$COQTOP/tools/coqdoc
+		    fsets_opt=yes
+		    fsets=all
 		    reals_opt=yes
 		    reals=all;;
     -src|--src) COQTOP=$2
@@ -97,6 +101,9 @@ while : ; do
     -opt|--opt) bytecamlc=ocamlc.opt
                 camlp4o=camlp4o  # can't add .opt since dyn load'll be required
                 nativecamlc=ocamlopt.opt;;
+    -fsets|--fsets) fsets_opt=yes
+                    fsets=$2
+		    shift;;
     -reals|--reals) reals_opt=yes
 		    reals=$2
 		    shift;;
@@ -219,6 +226,18 @@ case $coqdocdir_spec in
     yes) COQDOCDIR=$coqdocdir;;
 esac
 
+case $fsets_opt in
+    no) echo "Should I compile the complete theory of finite sets [Y/N, default is Y] ?"
+	read fsets_ans
+
+	case $fsets_ans in
+	    "N"|"n"|"No"|"NO"|"no")
+		    fsets=basic;;
+		*) fsets=all;;
+	esac;;
+    yes) true;;
+esac
+
 case $reals_opt in
     no) echo "Should I compile the complete theory of real analysis [Y/N, default is Y] ?"
 	read reals_ans
@@ -410,6 +429,11 @@ echo "  Objective-Caml/Camlp4 version     : $CAMLVERSION"
 echo "  Objective-Caml/Camlp4 binaries in : $CAMLBIN"
 echo "  Objective-Caml library in         : $CAMLLIB"
 echo "  Camlp4 library in                 : $CAMLP4LIB"
+if test "$fsets" = "all"; then
+echo "  FSets theory                      : All"
+else
+echo "  FSets theory                      : Basic"
+fi
 if test "$reals" = "all"; then
 echo "  Reals theory                      : All"
 else
@@ -523,6 +547,7 @@ sed -e "s|LOCALINSTALLATION|$local|" \
     -e "s|BYTECAMLC|$bytecamlc|" \
     -e "s|NATIVECAMLC|$nativecamlc|" \
     -e "s|STRIPCOMMAND|$STRIPCOMMAND|" \
+    -e "s|FSETSOPT|$fsets|" \
     -e "s|REALSOPT|$reals|" \
     -e "s|COQIDEOPT|$COQIDE|" \
       $COQTOP/config/Makefile.template > $COQTOP/config/Makefile