From 512f585d904fbfaedc515c1832227741fe1352d7 Mon Sep 17 00:00:00 2001 From: Adam Chlipala Date: Mon, 25 Apr 2016 09:00:28 -0400 Subject: [PATCH] SharedMemory: make work with Coq 8.5 --- SharedMemory.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/SharedMemory.v b/SharedMemory.v index b5475b0..9f4ad14 100644 --- a/SharedMemory.v +++ b/SharedMemory.v @@ -705,7 +705,7 @@ Proof. first_order; eauto. 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. eapply step_nextAction_other in H0; eauto; first_order; subst; try equality.