diff options
Diffstat (limited to 'src/translation/Veriloggenproof.v')
| -rw-r--r-- | src/translation/Veriloggenproof.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/src/translation/Veriloggenproof.v b/src/translation/Veriloggenproof.v index c83a3b1..59267f7 100644 --- a/src/translation/Veriloggenproof.v +++ b/src/translation/Veriloggenproof.v @@ -17,14 +17,18 @@ *) From compcert Require Import Smallstep Linking Integers Globalenvs. +From compcert Require Errors. From vericert Require HTL. From vericert Require Import Vericertlib Veriloggen Verilog ValueInt AssocMap. Require Import Lia. + Local Open Scope assocmap. Definition match_prog (prog : HTL.program) (tprog : Verilog.program) := - match_program (fun cu f tf => tf = transl_fundef f) eq prog tprog. + match_program (fun cu f tf => Errors.OK tf = transl_fundef prog f) eq prog tprog. + +(* Lemma transf_program_match: forall prog, match_prog prog (transl_program prog). @@ -404,3 +408,4 @@ Section CORRECTNESS. Qed. End CORRECTNESS. +*) |