diff options
Diffstat (limited to 'library/declaremods.ml')
| -rw-r--r-- | library/declaremods.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/library/declaremods.ml b/library/declaremods.ml index cf333a886..5866d612e 100644 --- a/library/declaremods.ml +++ b/library/declaremods.ml @@ -223,10 +223,10 @@ let conv_names_do_module exists what iter_objects i ((sp,kn),substobjs) = let dir = dir_of_sp sp and mp = mp_of_kn kn in do_module exists what iter_objects i dir mp substobjs [] -(* Interactive modules and module types cannot be recached! cache_mod* - functions can be called only once (and "end_mod*" set the flag to - false then) -*) +(* Nota: Interactive modules and module types cannot be recached! + This used to be checked here via a flag along the substobjs. + The check is still there for module types (see cache_modtype). *) + let cache_module ((sp,kn),substobjs) = let dir = dir_of_sp sp and mp = mp_of_kn kn in do_module false "cache" load_objects 1 dir mp substobjs [] |