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 | |
| parent | fe45801c1fdfebeacaf5daa0569d89838b11774f (diff) | |
blindage False_rec
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1634 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/extraction.ml | 4 | ||||
| -rw-r--r-- | contrib/extraction/test/Makefile | 8 | ||||
| -rwxr-xr-x | contrib/extraction/test/extract | 2 |
3 files changed, 9 insertions, 5 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index dafd0747a9..181d423daf 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -816,7 +816,11 @@ and extract_inductive_declaration sp = (*s Extraction of a global reference i.e. a constant or an inductive. *) +let false_rec_sp = path_of_string "Coq.Init.Specif.False_rec" +let false_rec_e = MLexn (id_of_string "False_rec") + let extract_declaration r = match r with + | ConstRef sp when sp = false_rec_sp -> Dglob (r, false_rec_e) | ConstRef sp -> (match extract_constant sp with | Emltype (mlt, s, vl) -> Dabbrev (r, List.rev vl, mlt) 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) |