From d298c7e78504850850af3f282af12b790d3cbf8a Mon Sep 17 00:00:00 2001
From: David Aspinall <da@inf.ed.ac.uk>
Date: Sun, 17 Feb 2008 12:40:06 +0000
Subject: New files.

---
 etc/coq/UndoFail.v | 117 +++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 117 insertions(+)
 create mode 100644 etc/coq/UndoFail.v

diff --git a/etc/coq/UndoFail.v b/etc/coq/UndoFail.v
new file mode 100644
index 00000000..7d8b557e
--- /dev/null
+++ b/etc/coq/UndoFail.v
@@ -0,0 +1,117 @@
+(* Default undo depth is 100 in Coq 8.1.  See trac #204 *)
+
+Lemma Foo : True.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+idtac.
+assert (NI : ~False).
+intros IX; auto.
+
+(* Process the script until here, then undo back 3 or 4 lines.
+   Notice that NI doesn't disappear. *)
\ No newline at end of file
-- 
cgit v1.2.3