diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-07-07 17:27:08 +0100 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-07-07 17:27:08 +0100 |
| commit | 8486b4c046914b1388b68fe906fe267108f84267 (patch) | |
| tree | 2a09eb912526825848fac77df54fe9e4917cd385 /src/Compiler.v | |
| parent | e63fef0613ed9e497279ae47b746413a093e9530 (diff) | |
| download | vericert-8486b4c046914b1388b68fe906fe267108f84267.tar.gz vericert-8486b4c046914b1388b68fe906fe267108f84267.zip | |
Fixes to operators
Diffstat (limited to 'src/Compiler.v')
| -rw-r--r-- | src/Compiler.v | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/Compiler.v b/src/Compiler.v index db3a810..d716caa 100644 --- a/src/Compiler.v +++ b/src/Compiler.v @@ -98,6 +98,7 @@ Definition transf_hls (p : Csyntax.program) : res Verilog.program := @@@ Cminorgen.transl_program @@@ Selection.sel_program @@@ RTLgen.transl_program + @@ print (print_RTL 0) @@@ transf_backend. Local Open Scope linking_scope. @@ -129,6 +130,7 @@ Proof. 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. destruct (Selection.sel_program p4) as [p5|e] eqn:P5; simpl in T; try discriminate. + rewrite ! compose_print_identity in T. destruct (RTLgen.transl_program p5) as [p6|e] eqn:P6; simpl in T; try discriminate. unfold transf_backend in T. simpl in T. rewrite ! compose_print_identity in T. destruct (Inlining.transf_program p6) as [p7|e] eqn:P7; simpl in T; try discriminate. |