Context Navigation

Ticket #204: UndoFail.v

File UndoFail.v, 1.0 KB (added by mccreight, 16 years ago)
example of undo failure

Line
1	Lemma Foo : True.
2	idtac.
3	idtac.
4	idtac.
5	idtac.
6	idtac.
7	idtac.
8	idtac.
9	idtac.
10	idtac.
11	idtac.
12	idtac.
13	idtac.
14	idtac.
15	idtac.
16	idtac.
17	idtac.
18	idtac.
19	idtac.
20	idtac.
21	idtac.
22	idtac.
23	idtac.
24	idtac.
25	idtac.
26	idtac.
27	idtac.
28	idtac.
29	idtac.
30	idtac.
31	idtac.
32	idtac.
33	idtac.
34	idtac.
35	idtac.
36	idtac.
37	idtac.
38	idtac.
39	idtac.
40	idtac.
41	idtac.
42	idtac.
43	idtac.
44	idtac.
45	idtac.
46	idtac.
47	idtac.
48	idtac.
49	idtac.
50	idtac.
51	idtac.
52	idtac.
53	idtac.
54	idtac.
55	idtac.
56	idtac.
57	idtac.
58	idtac.
59	idtac.
60	idtac.
61	idtac.
62	idtac.
63	idtac.
64	idtac.
65	idtac.
66	idtac.
67	idtac.
68	idtac.
69	idtac.
70	idtac.
71	idtac.
72	idtac.
73	idtac.
74	idtac.
75	idtac.
76	idtac.
77	idtac.
78	idtac.
79	idtac.
80	idtac.
81	idtac.
82	idtac.
83	idtac.
84	idtac.
85	idtac.
86	idtac.
87	idtac.
88	idtac.
89	idtac.
90	idtac.
91	idtac.
92	idtac.
93	idtac.
94	idtac.
95	idtac.
96	idtac.
97	idtac.
98	idtac.
99	idtac.
100	idtac.
101	idtac.
102	idtac.
103	idtac.
104	idtac.
105	idtac.
106	idtac.
107	idtac.
108	idtac.
109	idtac.
110	idtac.
111	assert (NI : ~False).
112	intros IX; auto.
113
114	(* Process the script until here, then undo back 3 or 4 lines.
115	Notice that NI doesn't disappear. *)