An error message instead of an empty extraction when the monolithic

extraction is given the name of a .v Module.



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

3 files changed, 13 insertions, 9 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index b8d964b85..b6367d98a 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -220,7 +220,7 @@ let rec extract_msb env mp all = function
 
 and extract_meb env mpo all = function 
   | MEBident mp -> 
-      if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp; 
+      if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false; 
       Visit.add_mp mp; MEident mp 
   | MEBapply (meb, meb',_) -> 
       MEapply (extract_meb env None true meb, 
@@ -380,8 +380,9 @@ let full_extraction f qualids =
     | q::l -> 
 	let refs,mps = find l in 
 	try 
-	  let mp = Nametab.locate_module (snd (qualid_of_reference q))
-	  in refs,(mp::mps)
+	  let mp = Nametab.locate_module (snd (qualid_of_reference q)) in 
+	  if is_modfile mp then error_MPfile_as_mod mp true; 
+	  refs,(mp::mps)
 	with Not_found -> (Nametab.global q)::refs, mps 
   in  
   let refs,mps = find qualids in
@@ -397,7 +398,8 @@ let full_extraction f qualids =
 let simple_extraction qid = 
   init false; 
   try 
-    let _ = Nametab.locate_module (snd (qualid_of_reference qid)) in 
+    let mp = Nametab.locate_module (snd (qualid_of_reference qid)) in 
+    if is_modfile mp then error_MPfile_as_mod mp true; 
     full_extraction None [qid]
   with Not_found -> 
     let r = Nametab.global qid in 
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml
index 7a8ff95ed..772a49742 100644
--- a/contrib/extraction/table.ml
+++ b/contrib/extraction/table.ml
@@ -287,11 +287,13 @@ let error_not_visible r =
        str "For example, it may be inside an applied functor." ++
        str "Use Recursive Extraction to get the whole environment.")
 
-let error_MPfile_as_mod mp = 
-  err (str ("The whole file "^(string_of_modfile mp)^
-	    ".v is used somewhere as a module.\n"^
+let error_MPfile_as_mod mp b = 
+  let s1 = if b then "asked" else "required" in 
+  let s2 = if b then "extract some objects of this module or\n" else "" in
+  err (str ("Extraction of file "^(string_of_modfile mp)^
+	    ".v as a module is "^s1^".\n"^
 	    "Monolithic Extraction cannot deal with this situation.\n"^
-	    "Please use (Recursive) Extraction Library instead.\n"))
+	    "Please "^s2^"use (Recursive) Extraction Library instead.\n"))
 
 let error_record r = 
   err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli
index 304e374b5..9e9d8c873 100644
--- a/contrib/extraction/table.mli
+++ b/contrib/extraction/table.mli
@@ -28,7 +28,7 @@ val error_module_clash : string -> 'a
 val error_unknown_module : qualid -> 'a
 val error_scheme : unit -> 'a
 val error_not_visible : global_reference -> 'a
-val error_MPfile_as_mod : module_path -> 'a
+val error_MPfile_as_mod : module_path -> bool -> 'a
 val error_record : global_reference -> 'a 
 val check_inside_module : unit -> unit
 val check_inside_section : unit -> unit