blob: c4826e0dce9f445757fdca3371c701b506dbce90 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
Module GoalGoal;
Goal first : {A:Prop}A->A;
intros; Immed;
(* no Save *)
Goal second : {A:Prop}A->A;
intros; Immed;
Save second;
(* asserting until here caused Proof General to swap first and second.
This is a bug for LEGO. Thanks to Martin Hofmann for pointing this
out. An obvious bug fix would be to make the function
proof-lift-global Coq specific. *)
|
