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
---
 test-suite/ide/undo.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'test-suite')

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