diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-29 16:22:18 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-09-29 17:08:56 +0200 |
| commit | b2fc9b55d9c59a9c507786a650377e2f0a1ddad8 (patch) | |
| tree | b6e835836c78566162d79c83bf353aa555a1d95c /kvx/Asmgenproof.v | |
| parent | 52b4f973646c3b79804fcdddeed5325ab1f3ce7d (diff) | |
| download | compcert-kvx-b2fc9b55d9c59a9c507786a650377e2f0a1ddad8.tar.gz compcert-kvx-b2fc9b55d9c59a9c507786a650377e2f0a1ddad8.zip | |
simpl -> cbn
Diffstat (limited to 'kvx/Asmgenproof.v')
| -rw-r--r-- | kvx/Asmgenproof.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kvx/Asmgenproof.v b/kvx/Asmgenproof.v index 9e35e268..636c105f 100644 --- a/kvx/Asmgenproof.v +++ b/kvx/Asmgenproof.v @@ -39,7 +39,7 @@ Proof. 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, Compopts.time in *. remember (Machblockgen.transf_program p) as mbp. - unfold match_prog; simpl. + unfold match_prog; cbn. exists mbp; split. apply Machblockgenproof.transf_program_match; auto. exists x; split. apply Asmblockgenproof.transf_program_match; auto. exists x0; split. apply PostpassSchedulingproof.transf_program_match; auto. @@ -72,7 +72,7 @@ Let tge := Genv.globalenv tprog. Theorem transf_program_correct: forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. - unfold match_prog in TRANSF. simpl in TRANSF. + unfold match_prog in TRANSF. cbn in TRANSF. inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H. eapply compose_forward_simulations. exploit Machblockgenproof.transf_program_correct; eauto. |