diff options
Diffstat (limited to 'mppa_k1c/Asmgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v index 5d7bb81f..7388f6da 100644 --- a/mppa_k1c/Asmgenproof.v +++ b/mppa_k1c/Asmgenproof.v @@ -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. unfold time in *. 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. |