diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-23 18:16:21 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-04-23 18:16:21 +0000 |
| commit | 7c56058bad50c783a24bfa2d7adf5e257198303a (patch) | |
| tree | b7d838436c6b9eb7f7db778a5e506c6c93f4287f /library/declaremods.ml | |
| parent | a672da543ac5ba589abb016e8f1cd8e448326fc3 (diff) | |
Fix issues with "Reset Initial" in scripts given to coqtop -l
Doing coqtop -l on a file starting with Reset Initial used to fail.
To avoid that, we now always place an initial DOT in the libstack.
Backtrack.reset_initial has been adapted accordingly: during an
interactive session following a Load via coqtop -l (or .coqrc),
a Reset Initial will bring back at the start of the interactive
session, *not* undoing the initial Load.
Note : Reset Initial might hence not be equivalent anymore to BackTo 1.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16449 85f007b7-540e-0410-9357-904b9bb8a0f7
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 [] |