From 7d3ab7e00453e259939535618e4e10c624a37ec9 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sun, 15 Feb 2015 19:03:18 +0100
Subject: Undo: back to 8.4 semantics (Close #3514)

Only tactics are taken into account.
---
 test-suite/output/simpl.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'test-suite/output')

diff --git a/test-suite/output/simpl.v b/test-suite/output/simpl.v
index 89638eedd7..5f1926f142 100644
--- a/test-suite/output/simpl.v
+++ b/test-suite/output/simpl.v
@@ -4,10 +4,10 @@ Goal forall x, 0+x = 1+x.
 intro x.
 simpl (_ + x).
 Show.
-Undo 2.
+Undo.
 simpl (_ + x) at 2.
 Show.
-Undo 2.
+Undo.
 simpl (0 + _).
 Show.
-Undo 2.
+Undo.
-- 
cgit v1.2.3