1 files changed, 11 insertions, 0 deletions
diff --git a/src/hls/Pipeline.v b/src/hls/Pipeline.v
new file mode 100644
index 0000000..ea0c32e
--- /dev/null
+++ b/src/hls/Pipeline.v
@@ -0,0 +1,11 @@
+From compcert Require Import
+     Maps
+     AST
+     RTL.
+
+Parameter pipeline : function -> function.
+
+Definition transf_fundef := transf_fundef pipeline.
+
+Definition transf_program : program -> program :=
+  transform_program transf_fundef.