diff options
| author | herbelin | 2000-11-10 17:11:20 +0000 |
|---|---|---|
| committer | herbelin | 2000-11-10 17:11:20 +0000 |
| commit | 284c71cdacffc36e12b491cb6ddec6c02f5b9d95 (patch) | |
| tree | 4c19e274687d28e9b7402e94e2abd5605821db48 | |
| parent | 108766703db1400ff30f2de8365da9a774eee46b (diff) | |
Bugs lies a la confusion load/open et a un open abusivement recursif dans library
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@841 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | library/library.ml | 14 |
1 files changed, 12 insertions, 2 deletions
diff --git a/library/library.ml b/library/library.ml index ca43096342..ce5934217d 100644 --- a/library/library.ml +++ b/library/library.ml @@ -86,7 +86,7 @@ let vo_magic_number = 0700 let (raw_extern_module, raw_intern_module) = System.raw_extern_intern vo_magic_number ".vo" -let segment_iter f = +let segment_rec_iter f = let rec apply = function | sp,Leaf obj -> f (sp,obj) | _,OpenedSection _ -> assert false @@ -97,6 +97,16 @@ let segment_iter f = in iter +let segment_iter f = + let rec apply = function + | sp,Leaf obj -> f (sp,obj) + | _,OpenedSection _ -> assert false + | _,ClosedSection (_,seg) -> () + | _,(FrozenState _ | Module _) -> () + and iter seg = + List.iter apply seg + in + iter (*s [open_module s] opens a module. The module [s] and all modules needed by [s] are assumed to be already loaded. When opening [s] we recursively open @@ -121,7 +131,7 @@ let rec open_module s = then same value as for caller is reused in recursive loadings). *) let load_objects decls = - segment_iter load_object decls + segment_rec_iter load_object decls let rec load_module_from s f = let (lpe,fname,ch) = raw_intern_module (get_load_path ()) f in |