diff options
| author | Enrico Tassi | 2015-02-23 17:14:05 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-02-23 17:14:05 +0100 |
| commit | e87ca456fb4cbe54f09e13f1e20d504d2699ac2b (patch) | |
| tree | 41b358ee2deb7c614e39f7db27368f9626c19778 /library | |
| parent | 28781f3fd6ae6e7f281f906721e8a028679ca089 (diff) | |
| parent | df2f50db3703b4f7f88f00ac382c7f3f1efaceb3 (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'library')
| -rw-r--r-- | library/assumptions.mli | 2 | ||||
| -rw-r--r-- | library/library.ml | 7 |
2 files changed, 6 insertions, 3 deletions
diff --git a/library/assumptions.mli b/library/assumptions.mli index 809e536b43..bb36a97259 100644 --- a/library/assumptions.mli +++ b/library/assumptions.mli @@ -27,7 +27,7 @@ module ContextObjectMap : Map.ExtS (** Collects all the objects on which a term directly relies, bypassing kernel opacity, together with the recursive dependence DAG of objects. - WARNING: some terms may not make sense in the environement, because they are + WARNING: some terms may not make sense in the environment, because they are sealed inside opaque modules. Do not try to do anything fancy with those terms apart from printing them, otherwise demons may fly out of your nose. *) diff --git a/library/library.ml b/library/library.ml index e4169d66e0..95b817d0a1 100644 --- a/library/library.ml +++ b/library/library.ml @@ -587,8 +587,11 @@ let import_module export modl = | [] -> () | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in let rec aux acc = function - | m :: l -> - (match safe_locate_module m with + | (loc,dir as m) :: l -> + let m,acc = + try Nametab.locate_module dir, acc + with Not_found-> flush acc; safe_locate_module m, [] in + (match m with | MPfile dir -> aux (dir::acc) l | mp -> flush acc; Declaremods.import_module export mp; aux [] l) | [] -> flush acc |