From ee4c7b812c9a2eefbf44097f9168ca1c55c2e668 Mon Sep 17 00:00:00 2001
From: courtieu
Date: Wed, 23 Apr 2008 11:43:58 +0000
Subject: Added frozen state after each command.

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

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 75d1cdc99b..ac834b2a58 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -197,10 +197,12 @@ and read_vernac_file verbosely s =
 (* raw_do_vernac : char Stream.t -> unit
  * parses and executes one command of the vernacular char stream.
  * Marks the end of the command in the lib_stk with a new label to
- * make vernac undoing easier. *)
+ * make vernac undoing easier. Also freeze state to speed up
+ * backtracking. *)
 
 let raw_do_vernac po =
   vernac (States.with_heavy_rollback Vernacentries.interp) (po,None);
+  Lib.add_frozen_state();
   Lib.mark_end_of_command()
 
 (* XML output hooks *)
-- 
cgit v1.2.3