BIG MAJ Extraction:

------------------
- (Recursive) Extraction Module devient (Recursive) Extraction Library
  (pour cause d'ambiguite avec les nouveaux modules Coq).
- un nouveau Extraction Module qui extrait dans le toplevel tout module Coq
- tout fixpoint est de nouveau inlinable (Yves).
- fix bug du calcul d'env minimal des modules en extraction monolithique.
- un nouveau fichier Modutil regroupant manques de Modops & functions
  specifiques aux modules MiniML
- plus d'aliases a trainer (mais des substitutions des le depart)
- ET SURTOUT: un nommage correct (ou du moins moins pire) dans les modtypes
  et les functors.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3934 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 2 insertions, 2 deletions

diff --git a/contrib/extraction/test/extract b/contrib/extraction/test/extract
index 2b96f354f..83444be31 100755
--- a/contrib/extraction/test/extract
+++ b/contrib/extraction/test/extract
@@ -4,7 +4,7 @@ vfile=`./ml2v $1`
 d=`dirname $vfile`
 n=`basename $vfile .v`
 if [ -e custom/$n ]; then cat custom/$n > /tmp/extr$$.v; fi  
-echo "Cd \"$d\". Extraction Module $n. " >> /tmp/extr$$.v
+echo "Cd \"$d\". Extraction Library $n. " >> /tmp/extr$$.v
 ../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v 
 out=$?
 rm -f /tmp/extr$$.v
diff --git a/contrib/extraction/test/extract.haskell b/contrib/extraction/test/extract.haskell
index 3f4a59d49..d11bc706e 100755
--- a/contrib/extraction/test/extract.haskell
+++ b/contrib/extraction/test/extract.haskell
@@ -4,7 +4,7 @@ vfile=`./hs2v $1`
 d=`dirname $vfile`
 n=`basename $vfile .v`
 if [ -e custom/$n ]; then cat custom/$n > /tmp/extr$$.v; fi  
-echo "Cd \"$d\". Extraction Language Haskell. Extraction Module $n. " >> /tmp/extr$$.v
+echo "Cd \"$d\". Extraction Language Haskell. Extraction Library $n. " >> /tmp/extr$$.v
 ../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v 
 out=$?
 rm -f /tmp/extr$$.v