diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-07 13:12:39 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2019-09-07 13:12:39 +0200 |
| commit | 4cdd085383c5e18989b8636455ddcfc7ceb5843a (patch) | |
| tree | 43bb51452db0957915a5e9818b0af78b20fb048b /backend/Stackingproof.v | |
| parent | 35febfa5b231a71234a1b32c128169352e96eaca (diff) | |
| download | compcert-kvx-4cdd085383c5e18989b8636455ddcfc7ceb5843a.tar.gz compcert-kvx-4cdd085383c5e18989b8636455ddcfc7ceb5843a.zip | |
fixes for compiling on other platforms
Diffstat (limited to 'backend/Stackingproof.v')
| -rw-r--r-- | backend/Stackingproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index 19a40e0f..d3fcdb91 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1943,7 +1943,7 @@ Proof. { econstructor; split. apply plus_one. apply exec_Mload with (a:=a') (v:=v'); eauto. - try (rewrite <- A; apply eval_addressing_preserved; assumption). + try (rewrite <- A; apply eval_addressing_preserved; auto; exact symbols_preserved). econstructor; eauto with coqlib. apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. apply agree_locs_set_reg. apply agree_locs_undef_locs. auto. apply destroyed_by_load_caller_save. auto. @@ -1951,7 +1951,7 @@ Proof. { econstructor; split. apply plus_one. apply exec_Mload_notrap2 with (a:=a'); eauto. - try (rewrite <- A; apply eval_addressing_preserved; assumption). + try (rewrite <- A; apply eval_addressing_preserved; auto; exact symbols_preserved). econstructor; eauto with coqlib. apply agree_regs_set_reg. rewrite transl_destroyed_by_load. apply agree_regs_undef_regs; auto. auto. |