pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-12-01 00:26:18 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Fix for Coq 8.5 again

Browse source
This commit is contained in:
Adam Chlipala 2017-02-07 21:35:23 -05:00
parent 466ea72b27
commit 0e68042f07
2 changed files with 2 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
LambdaCalculusAndTypeSoundness.v
View file

@ -651,11 +651,7 @@ Module Stlc.
| [ H : step _ _ |- _ ] => invert H | [ H : step _ _ |- _ ] => invert H
end. end.
right. right.
exists (Plus x e2).
eapply StepRule with (C := Plus1 C e2).
eauto. eauto.
eauto.
assumption.
match goal with match goal with
| [ H : exists x, _ |- _ ] => invert H | [ H : exists x, _ |- _ ] => invert H
@ -664,11 +660,7 @@ Module Stlc.
| [ H : step _ _ |- _ ] => invert H | [ H : step _ _ |- _ ] => invert H
end. end.
right. right.
exists (Plus e1 x).
eapply StepRule with (C := Plus2 e1 C).
eauto. eauto.
eauto.
assumption.
match goal with match goal with
| [ H : exists x, step e1 _ |- _ ] => invert H | [ H : exists x, step e1 _ |- _ ] => invert H
@ -706,11 +698,7 @@ Module Stlc.
| [ H : step _ _ |- _ ] => invert H | [ H : step _ _ |- _ ] => invert H
end. end.
right. right.
exists (App x e2).
eapply StepRule with (C := App1 C e2).
eauto. eauto.
eauto.
assumption.
match goal with match goal with
| [ H : exists x, _ |- _ ] => invert H | [ H : exists x, _ |- _ ] => invert H
@ -719,11 +707,7 @@ Module Stlc.
| [ H : step _ _ |- _ ] => invert H | [ H : step _ _ |- _ ] => invert H
end. end.
right. right.
exists (App e1 x).
eapply StepRule with (C := App2 e1 C).
eauto. eauto.
eauto.
assumption.
match goal with match goal with
| [ H : exists x, step e1 _ |- _ ] => invert H | [ H : exists x, step e1 _ |- _ ] => invert H

4
TypesAndMutation.v
View file

@ -304,10 +304,10 @@ Module References.
Proof. Proof.
induct 2; t. induct 2; t.
match goal with match goal with
| [ H1 : _ = Some _, H2 : forall l : loc, _ |- _ ] => apply H3 in H8; t | [ H1 : _ = Some _, H2 : forall l : loc, _ |- _ ] => apply H2 in H1; t
end. end.
match goal with match goal with
| [ H1 : _ = Some _, H2 : forall l : loc, _ |- _ ] => apply H3 in H8; t | [ H1 : _ = Some _, H2 : forall l : loc, _ |- _ ] => apply H2 in H1; t
end. end.
Qed. Qed.