diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-22 11:27:15 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-22 11:27:15 +0200 |
| commit | c991b6f67778634cf1c8df5fb429a74d068c8fb8 (patch) | |
| tree | 35122478bd70025426c0d449f75b81a9cf85012d /driver | |
| parent | 05a5825ee55227327ba1b09a548e3b9ba876d0cf (diff) | |
| download | compcert-kvx-c991b6f67778634cf1c8df5fb429a74d068c8fb8.tar.gz compcert-kvx-c991b6f67778634cf1c8df5fb429a74d068c8fb8.zip | |
cbn and copyright
Diffstat (limited to 'driver')
| -rw-r--r-- | driver/Compiler.vexpand | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/driver/Compiler.vexpand b/driver/Compiler.vexpand index 1e671464..0f59aab7 100644 --- a/driver/Compiler.vexpand +++ b/driver/Compiler.vexpand @@ -208,15 +208,15 @@ Theorem transf_c_program_match: match_prog p tp. Proof. intros p tp T. - unfold transf_c_program, time in T. simpl in T. - destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; simpl in T; try discriminate. - unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; simpl in T; try discriminate. - destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; simpl in T; try discriminate. - destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; simpl in T; try discriminate. - unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. simpl in T. - destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. - destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. + unfold transf_c_program, time in T. cbn in T. + destruct (SimplExpr.transl_program p) as [p1|e] eqn:P1; cbn in T; try discriminate. + unfold transf_clight_program, time in T. rewrite ! compose_print_identity in T. cbn in T. + destruct (SimplLocals.transf_program p1) as [p2|e] eqn:P2; cbn in T; try discriminate. + destruct (Cshmgen.transl_program p2) as [p3|e] eqn:P3; cbn in T; try discriminate. + destruct (Cminorgen.transl_program p3) as [p4|e] eqn:P4; cbn in T; try discriminate. + unfold transf_cminor_program, time in T. rewrite ! compose_print_identity in T. cbn in T. + destruct (Selection.sel_program p4) as [p5|e] eqn:P5; cbn in T; try discriminate. + destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; cbn in T; try discriminate. unfold transf_rtl_program, time in T. rewrite ! compose_print_identity in T. cbn in T. EXPAND_RTL_PROOF |