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/extract_env.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/extract_env.ml')
| -rw-r--r-- | contrib/extraction/extract_env.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index c231dc4f28..0ef993057a 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 |