diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-21 13:41:53 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-21 13:41:53 +0000 |
| commit | 1d6a9cd4ac13b69d1aa5b06f7046685f2fe400ba (patch) | |
| tree | bd3b2db94703cbbf7e67bb18493bcddd130e5ab3 /contrib/extraction/extract_env.ml | |
| parent | f67216f5fd47881a181dc32e7d67b4210dacf54e (diff) | |
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
Diffstat (limited to 'contrib/extraction/extract_env.ml')
| -rw-r--r-- | contrib/extraction/extract_env.ml | 10 |
1 files changed, 6 insertions, 4 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 |