Remove unnecessary examples from HTL

2 files changed, 5 insertions, 10 deletions

diff --git a/src/translation/HTLgen.v b/src/translation/HTLgen.v
index 9c2e168..d7f88c1 100644
--- a/src/translation/HTLgen.v
+++ b/src/translation/HTLgen.v
@@ -17,8 +17,8 @@
  *)
 
 From coqup Require Import HTL Coquplib.
-From compcert Require Import Maps.
 
+From compcert Require Import Maps.
 From compcert Require Errors.
 From compcert Require Import AST RTL.
 
@@ -179,11 +179,6 @@ Definition transf_function (f: function) : Errors.res module :=
   | Error err => Errors.Error err
   end.
 
-Definition example : mon HTL.code := PTree.traverse transf_instr
-  (PTree.set 2%positive (RTL.Icall sig ros args res n) (PTree.set 1%positive (RTL.Iop (Op.Omove) nil 1%positive 2%positive) (PTree.empty RTL.instruction))).
-
-Compute example.
-
 Definition transf_fundef (fd: fundef) : Errors.res moddecl :=
   transf_partial_fundef transf_function fd.
 
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).