From 64e5ee718e55e13473bd3103a9535aa76ec4c63d Mon Sep 17 00:00:00 2001
From: vgross
Date: Tue, 23 Mar 2010 11:13:20 +0000
Subject: Fix bug in backtracking.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12876 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 ide/coq.ml            | 2 +-
 test-suite/ide/undo.v | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/ide/coq.ml b/ide/coq.ml
index ac978e4cfa..4c5179edd5 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -461,7 +461,7 @@ struct
     List.iter
       (fun cmd -> 
          let str = (if value then "Set" else "Unset") ^ " Printing " ^ cmd ^ "." in
-         Vernac.eval_ctrl (snd (Vernac.parse_sentence (parsable_of_string str,None))))
+         Vernac.eval_expr (Vernac.parse_sentence (parsable_of_string str,None)))
       opt
 
   let enforce_hack () = Hashtbl.iter set state_hack 
diff --git a/test-suite/ide/undo.v b/test-suite/ide/undo.v
index d5e9ee5e82..84eacc3e34 100644
--- a/test-suite/ide/undo.v
+++ b/test-suite/ide/undo.v
@@ -3,8 +3,8 @@
 
 (* Undoing arbitrary commands, as first step *)
 
-Theorem a : O=O.
-Ltac f x := x.
+Theorem a : O=O. (* 2 *)
+Ltac f x := x. (* 1 * 3 *)
 assert True by trivial.
 trivial.
 Qed.
-- 
cgit v1.2.3