diff options
Diffstat (limited to 'mppa_k1c/Asmgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index e7e21a18..7388f6da 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -10,7 +10,7 @@ (* *) (* *********************************************************************) -(** Correctness proof for RISC-V generation: main proof. *) +(** Correctness proof for Asmgen *) Require Import Coqlib Errors. Require Import Integers Floats AST Linking. @@ -35,7 +35,7 @@ Proof. intros p tp H. unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H. inversion_clear H. apply bind_inversion in H1. destruct H1. - inversion_clear H. inversion H2. remember (Machblockgen.transf_program p) as mbp. + inversion_clear H. inversion H2. unfold time, Compopts.time in *. remember (Machblockgen.transf_program p) as mbp. unfold match_prog; simpl. exists mbp; split. apply Machblockgenproof.transf_program_match; auto. exists x; split. apply Asmblockgenproof.transf_program_match; auto. @@ -89,4 +89,4 @@ Module Asmgenproof0. Definition return_address_offset := return_address_offset. -End Asmgenproof0.
\ No newline at end of file +End Asmgenproof0. |