aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--src/Compiler.v2
1 files changed, 0 insertions, 2 deletions
diff --git a/src/Compiler.v b/src/Compiler.v
index 7b17336..6efd7a2 100644
--- a/src/Compiler.v
+++ b/src/Compiler.v
@@ -88,8 +88,6 @@ Definition transf_backend (r : RTL.program) : res Verilog.program :=
@@ print print_HTL
@@ Veriloggen.transl_program.
-Check mkpass.
-
Definition transf_hls (p : Csyntax.program) : res Verilog.program :=
OK p
@@@ SimplExpr.transl_program