Merge branch 'michalis' of https://github.com/mpardalos/vericert into michalis-merge

1 files changed, 14 insertions, 0 deletions

diff --git a/src/hls/Verilog.v b/src/hls/Verilog.v
index a7db3ba..ca5abd4 100644
--- a/src/hls/Verilog.v
+++ b/src/hls/Verilog.v
@@ -251,6 +251,20 @@ Definition posToLit (p : positive) : expr :=
 Definition fext := unit.
 Definition fextclk := nat -> fext.
 
+Definition map_body (f : list module_item -> list module_item) (m : module) :=
+  mkmodule
+    (mod_start m)
+    (mod_reset m)
+    (mod_clk m)
+    (mod_finish m)
+    (mod_return m)
+    (mod_st m)
+    (mod_stk m)
+    (mod_stk_len m)
+    (mod_args m)
+    (f (mod_body m))
+    (mod_entrypoint m).
+
 (** ** State
 
 The [state] contains the following items: