diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-09 21:47:36 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-09 21:47:36 +0000 |
| commit | 29c800d48a84e89f2db8a60c64b3f91b59b54384 (patch) | |
| tree | e7fd2a44358ee8286739d9dbf9fea1406d0124ea | |
| parent | 962f845da900095720f93b97c3977be96027c82b (diff) | |
Extraction now checks that the required libraries are indeed loaded (bug #1144)
If a library is Require'd from inside an "opaque" Module (e.g. a module with
an interface given by a ":"), then the required library is not loaded anymore
after closing this module. We add an error in this situation, asking the user
to manually do a Require before performing the Extraction.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10208 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/extraction/extract_env.ml | 3 | ||||
| -rw-r--r-- | contrib/extraction/table.ml | 6 | ||||
| -rw-r--r-- | contrib/extraction/table.mli | 1 |
3 files changed, 8 insertions, 2 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index c231dc4f2..0ef993057 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -92,7 +92,8 @@ module Visit : VISIT = struct let needed_kn kn = KNset.mem kn v.kn let needed_con c = Cset.mem c v.con let needed_mp mp = MPset.mem mp v.mp - let add_mp mp = v.mp <- MPset.union (prefixes_mp mp) v.mp + let add_mp mp = + check_loaded_modfile mp; v.mp <- MPset.union (prefixes_mp mp) v.mp let add_kn kn = v.kn <- KNset.add kn v.kn; add_mp (modpath kn) let add_con c = v.con <- Cset.add c v.con; add_mp (con_modpath c) let add_ref = function diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 0b2837e32..204319099 100644 --- a/contrib/extraction/table.ml +++ b/contrib/extraction/table.ml @@ -60,7 +60,6 @@ let at_toplevel mp = let visible_kn kn = at_toplevel (base_mp (modpath kn)) let visible_con kn = at_toplevel (base_mp (con_modpath kn)) - (*S The main tables: constants, inductives, records, ... *) (*s Constants tables. *) @@ -212,6 +211,11 @@ let error_record r = err (str "Record " ++ pr_global r ++ str " has an anonymous field." ++ fnl () ++ str "To help extraction, please use an explicit name.") +let check_loaded_modfile mp = match base_mp mp with + | MPfile dp -> if not (Library.library_is_loaded dp) then + err (str ("Please load library "^(string_of_dirpath dp^" first."))) + | _ -> () + (*S The Extraction auxiliary commands *) (*s Extraction AutoInline *) diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index 7bd2297cd..55402d94a 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -32,6 +32,7 @@ val error_MPfile_as_mod : dir_path -> 'a val error_record : global_reference -> 'a val check_inside_module : unit -> unit val check_inside_section : unit -> unit +val check_loaded_modfile : module_path -> unit (*s utilities concerning [module_path]. *) |