From d556fd3ffb8b59e2a5136ab748a3a8d73c3f45f0 Mon Sep 17 00:00:00 2001
From: courtieu
Date: Thu, 28 Dec 2006 15:41:39 +0000
Subject: Cleaning backtracking code, optimized "Backtrack n x y" when n is
 current state.

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

(limited to 'toplevel')

diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 185bfd93c8..4090748b3b 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -195,8 +195,8 @@ 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 to make vernac undoing
- * easier. *)
+ * Marks the end of the command in the lib_stk with a new label to
+ * make vernac undoing easier. *)
 
 let raw_do_vernac po =
   vernac (States.with_heavy_rollback Vernacentries.interp) (po,None);
-- 
cgit v1.2.3