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

SharedMemory: make work with Coq 8.5

Browse source
This commit is contained in:
Adam Chlipala 2016-04-25 09:00:28 -04:00
parent 4744a4039c
commit 512f585d90
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
SharedMemory.v
View file

@ -705,7 +705,7 @@ Proof.
first_order; eauto. first_order; eauto.
eapply step_nextAction_other in H0; eauto; first_order; subst; try equality. eapply step_nextAction_other in H0; eauto; first_order; subst; try equality.
eapply commutes_sound' with (c2 := c2) (c1 := Write a v) in H3; eauto. eapply commutes_sound' with (c2 := c2) (c1 := Write a v) in H; eauto; try solve [ simplify; sets ].
first_order; eauto. first_order; eauto.
eapply step_nextAction_other in H0; eauto; first_order; subst; try equality. eapply step_nextAction_other in H0; eauto; first_order; subst; try equality.