aboutsummaryrefslogtreecommitdiffstats
path: root/src/Compiler.v
diff options
context:
space:
mode:
Diffstat (limited to 'src/Compiler.v')
-rw-r--r--src/Compiler.v1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/Compiler.v b/src/Compiler.v
index d99ce56..e837e9d 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -82,6 +82,7 @@ We then need to declare the external OCaml functions used to print out intermedi
Parameter print_RTL: Z -> RTL.program -> unit.
Parameter print_HTL: HTL.program -> unit.
Parameter print_RTLBlock: Z -> RTLBlock.program -> unit.
+Parameter print_RTLPar: Z -> RTLPar.program -> unit.
Definition print {A: Type} (printer: A -> unit) (prog: A) : A :=
let unused := printer prog in prog.