aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorletouzey2008-04-15 00:12:06 +0000
committerletouzey2008-04-15 00:12:06 +0000
commit324fd302e2c95a8b2f992aa967cc6dbac5665c4b (patch)
tree4aef563a2f5e66257365986aa69ea56ddb6adcba
parentc3396d4de820a223666ba78e88adbd744f0dc2ad (diff)
fix some bogus calls to id_of_string by the extraction
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10794 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--contrib/extraction/extract_env.ml13
1 files changed, 10 insertions, 3 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 445a26c729..e52571aadb 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -324,17 +324,24 @@ let descr () = match lang () with
(* From a filename string "foo.ml" or "foo", builds "foo.ml" and "foo.mli"
Works similarly for the other languages. *)
+let default_id = id_of_string "Main"
+
let mono_filename f =
let d = descr () in
match f with
- | None -> None, None, id_of_string "Main"
+ | None -> None, None, default_id
| Some f ->
let f =
if Filename.check_suffix f d.file_suffix then
Filename.chop_suffix f d.file_suffix
else f
- in
- Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id_of_string f
+ in
+ let id =
+ if lang () <> Haskell then default_id
+ else try id_of_string (Filename.basename f)
+ with _ -> error "Extraction: provided filename is not a valid identifier"
+ in
+ Some (f^d.file_suffix), Option.map ((^) f) d.sig_suffix, id
(* Builds a suitable filename from a module id *)