diff options
| author | Thomas Kleymann | 1998-10-18 14:24:06 +0000 |
|---|---|---|
| committer | Thomas Kleymann | 1998-10-18 14:24:06 +0000 |
| commit | b73c530b8230de54b0b3866e1cd77784d961528e (patch) | |
| tree | 938ec1156e38a7e38e03d073417b072707fed0e8 /etc | |
| parent | bb0b35e13e222ceffee83d49ec676c8b88c51966 (diff) | |
support for nested goals is now restricted to Coq
Diffstat (limited to 'etc')
| -rw-r--r-- | etc/lego/GoalGoal.l | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/etc/lego/GoalGoal.l b/etc/lego/GoalGoal.l new file mode 100644 index 00000000..c4826e0d --- /dev/null +++ b/etc/lego/GoalGoal.l @@ -0,0 +1,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. *)
\ No newline at end of file |