From 7c56058bad50c783a24bfa2d7adf5e257198303a Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 23 Apr 2013 18:16:21 +0000 Subject: 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 --- library/declaremods.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'library/declaremods.ml') 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 [] -- cgit v1.2.3