From 4cdd085383c5e18989b8636455ddcfc7ceb5843a Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Sat, 7 Sep 2019 13:12:39 +0200 Subject: fixes for compiling on other platforms --- backend/CSEproof.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'backend/CSEproof.v') diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 209fa40f..5bbb7508 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -1151,7 +1151,7 @@ Proof. econstructor. split. eapply exec_Iload; eauto. - try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption). + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). econstructor; eauto. eapply analysis_correct_1; eauto. simpl; eauto. @@ -1202,7 +1202,7 @@ Proof. { econstructor. split. eapply exec_Iload; eauto. - try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption). + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). econstructor; eauto. eapply analysis_correct_1; eauto. simpl; eauto. @@ -1216,7 +1216,7 @@ Proof. { econstructor. split. eapply exec_Iload_notrap2; eauto. - try (rewrite eval_addressing_preserved with (ge1 := ge) by assumption). + try (rewrite eval_addressing_preserved with (ge1 := ge); auto; exact symbols_preserved). econstructor; eauto. eapply analysis_correct_1; eauto. simpl; eauto. -- cgit