pl/frap
1
0
Fork 0
mirror of https://github.com/achlipala/frap.git synced 2024-11-10 00:07:51 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Working again with Coq 8.6.1

Browse source
This commit is contained in:
Adam Chlipala 2017-11-18 12:15:15 -05:00
parent e8c1980257
commit c6cc13587c
2 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
CompilerCorrectness.v
View file

@ -351,7 +351,7 @@ Proof.
eapply plug_deterministic in H0; eauto. eapply plug_deterministic in H0; eauto.
invert H0. invert H0.
match goal with match goal with
| [ H : step0 _ l' _ |- _ ] => eapply deterministic0 in H; eauto | [ H : step0 _ _ _, H' : step0 _ _ _ |- _ ] => eapply deterministic0 in H; [ | apply H' ]
end. end.
propositional; subst; auto. propositional; subst; auto.
invert H0. invert H0.

2
CompilerCorrectness_template.v
View file

@ -281,7 +281,7 @@ Proof.
eapply plug_deterministic in H0; eauto. eapply plug_deterministic in H0; eauto.
invert H0. invert H0.
match goal with match goal with
| [ H : step0 _ l' _ |- _ ] => eapply deterministic0 in H; eauto | [ H : step0 _ _ _, H' : step0 _ _ _ |- _ ] => eapply deterministic0 in H; [ | apply H' ]
end. end.
propositional; subst; auto. propositional; subst; auto.
invert H0. invert H0.