diff options
Diffstat (limited to 'contrib/extraction')
-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]. *) |