From fc507c51aba9e0258e41e3ea4c8b38bf2cc0dc1b Mon Sep 17 00:00:00 2001
From: bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 13 Feb 2001 07:40:31 +0000
Subject: Make sure the initial state used in a protected loop is the state
 chose exactly at the time the protected loop was started.  This makes it
 possible to have modifications of commands specific to the protected loop
 remembered throughout the session.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1371 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/toplevel.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 35dde0bcf..ca5e27e11 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.ml
@@ -292,7 +292,9 @@ let rec coq_switch b =
       protected_loop stdin
   with
     | Vernacinterp.Drop -> ()
-    | Vernacinterp.ProtectedLoop -> coq_switch false
+    | Vernacinterp.ProtectedLoop -> 
+	Lib.declare_initial_state();
+	coq_switch false
     | End_of_input -> mSGERRNL [<>]; pp_flush(); exit 0
     | Vernacinterp.Quit -> exit 0
     | e ->
-- 
cgit v1.2.3