diff options
| author | filliatr | 2001-04-19 15:07:41 +0000 |
|---|---|---|
| committer | filliatr | 2001-04-19 15:07:41 +0000 |
| commit | 8a009c8729dd6905dd7d47877b444fa38dd2e221 (patch) | |
| tree | 70f689960f99506af4f3d56796ea972e47193f21 /contrib/extraction/test | |
| parent | fe45801c1fdfebeacaf5daa0569d89838b11774f (diff) | |
blindage False_rec
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1634 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/test')
| -rw-r--r-- | contrib/extraction/test/Makefile | 8 | ||||
| -rwxr-xr-x | contrib/extraction/test/extract | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile index 2a29f866ac..994d7cf2c7 100644 --- a/contrib/extraction/test/Makefile +++ b/contrib/extraction/test/Makefile @@ -31,7 +31,8 @@ allcmo: .names.cmo $(CMONAMES) .names.ml: Makefile v2ml rm -f .names.ml; \ echo "MLNAMES= \\" > .names.ml; \ - find theories -name \*.v -exec ./v2ml \{\} \; | \ + V2ML=`pwd`/v2ml; \ + (cd $(TOPDIR); find theories -name \*.v -exec $$V2ML \{\} \;) | \ sed -e "s/\.ml/.ml \\\\/" >> .names.ml .names.cmo: .names.ml @@ -39,9 +40,8 @@ allcmo: .names.cmo $(CMONAMES) sed -e "1s/ML/CMO/" -e "s/\.ml/.cmo/" < .names.ml > .names.cmo tree: - for f in `cd $(TOPDIR); find theories -name \*.v`; do \ - mkdir -p `dirname $$f`; \ - cp $(TOPDIR)/$$f $$f; \ + for f in `cd $(TOPDIR); find theories -type d ! -name CVS`; do \ + mkdir -p $$f; \ done ml2v: ml2v.ml diff --git a/contrib/extraction/test/extract b/contrib/extraction/test/extract index 1b0886a7e9..b5d6a6a787 100755 --- a/contrib/extraction/test/extract +++ b/contrib/extraction/test/extract @@ -3,6 +3,6 @@ rm -f /tmp/extr.v d=`dirname $1` n=`basename $1 .v` echo "Cd \"$d\". Extraction Module $n. " > /tmp/extr$$.v;\ -(../../../bin/coqtop.opt -batch -require $n -load-vernac-source /tmp/extr$$.v && rm -f /tmp/extr$$.v) || (rm -f /tmp/extr$$.v; exit 1) +(../../../bin/coqtop.opt -silent -batch -require $n -load-vernac-source /tmp/extr$$.v && rm -f /tmp/extr$$.v) || (rm -f /tmp/extr$$.v; exit 1) |