diff options
Diffstat (limited to 'riscV/Asmgenproof.v')
| -rw-r--r-- | riscV/Asmgenproof.v | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 798dad9f..0d3c8042 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -816,6 +816,7 @@ Local Transparent destroyed_by_op. (* match states *) econstructor; eauto. apply agree_set_other; auto with asmgen. + apply agree_set_other; auto with asmgen. Simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. - (* Mbuiltin *) |