scripts; extraction False_rec

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

3 files changed, 3 insertions, 3 deletions

diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml
index 181d423da..29941f617 100644
--- a/contrib/extraction/extraction.ml
+++ b/contrib/extraction/extraction.ml
@@ -817,7 +817,7 @@ 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 false_rec_e = MLlam (prop_name, 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)
diff --git a/contrib/extraction/test/Makefile b/contrib/extraction/test/Makefile
index 994d7cf2c..bfc5ad0e5 100644
--- a/contrib/extraction/test/Makefile
+++ b/contrib/extraction/test/Makefile
@@ -10,7 +10,7 @@ INCL= -I theories/Arith \
 -I theories/Relations \
 -I theories/Sets \
 -I theories/Wellfounded \
--I theories/Zarith
+-I theories/ZArith
 
 
 MLNAMES=
diff --git a/contrib/extraction/test/ml2v.ml b/contrib/extraction/test/ml2v.ml
index f891b40ff..2cf9190e1 100644
--- a/contrib/extraction/test/ml2v.ml
+++ b/contrib/extraction/test/ml2v.ml
@@ -4,7 +4,7 @@ let _ =
     let fml = Sys.argv.(1) in
     let f = Filename.chop_extension fml in 
     let fv = f ^ ".v" in
-    if Sys.file_exists fv then
+    if Sys.file_exists ("../../../" ^ fv) then
       print_endline fv
     else
       let d = Filename.dirname f in