diff options
| author | letouzey | 2007-10-09 21:47:36 +0000 |
|---|---|---|
| committer | letouzey | 2007-10-09 21:47:36 +0000 |
| commit | 29c800d48a84e89f2db8a60c64b3f91b59b54384 (patch) | |
| tree | e7fd2a44358ee8286739d9dbf9fea1406d0124ea /contrib/extraction/table.ml | |
| 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
Diffstat (limited to 'contrib/extraction/table.ml')
| -rw-r--r-- | contrib/extraction/table.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/contrib/extraction/table.ml b/contrib/extraction/table.ml index 0b2837e322..2043190991 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 *) |