(* 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. *)