diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2008-02-17 12:40:06 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2008-02-17 12:40:06 +0000 |
| commit | d298c7e78504850850af3f282af12b790d3cbf8a (patch) | |
| tree | ce0569ba1ad6bb1741df96a7a781675bf86ba345 /etc/coq | |
| parent | a4e9483cd94c3f6f933dd52116bdd63f12970f6c (diff) | |
New files.
Diffstat (limited to 'etc/coq')
| -rw-r--r-- | etc/coq/UndoFail.v | 117 |
1 files changed, 117 insertions, 0 deletions
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 |