diff options
author | Yann Herklotz <git@yannherklotz.com> | 2020-03-29 16:41:09 +0100 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2020-03-29 16:41:09 +0100 |
commit | 65f30c5524280b5639a94674828986f0635b2477 (patch) | |
tree | be05fd2acf456773a02dbc8a61135f9c187bc46e /src/verilog/HTL.v | |
parent | c3106c7a61ecb79c1f1be0922aef32dffc92cc41 (diff) | |
download | vericert-kvx-65f30c5524280b5639a94674828986f0635b2477.tar.gz vericert-kvx-65f30c5524280b5639a94674828986f0635b2477.zip |
Remove unnecessary examples from HTL
Diffstat (limited to 'src/verilog/HTL.v')
-rw-r--r-- | src/verilog/HTL.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/verilog/HTL.v b/src/verilog/HTL.v index 202a8b7..f2620a7 100644 --- a/src/verilog/HTL.v +++ b/src/verilog/HTL.v @@ -60,19 +60,19 @@ Definition modsig (md : moddecl) := | AST.External ef => AST.ef_sig ef end. -(** Describes the transformation of VTL instruction by instruction. This applies +(** Describes various transformations that can be applied to HTL. This applies the transformation to each instruction in the function and returns the new function with the modified instructions. *) Section TRANSF. - Variable transf : node -> instruction -> instruction. + Variable transf_instr : node -> instruction -> instruction. - Definition transf_function (m : module) : module := + Definition transf_module (m : module) : module := mkmodule m.(mod_sig) m.(mod_params) m.(mod_stacksize) - (PTree.map transf m.(mod_code)) + (PTree.map transf_instr m.(mod_code)) m.(mod_insts) m.(mod_entrypoint). |