diff options
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 |