aboutsummaryrefslogtreecommitdiffstats
path: root/src/Compiler.v
diff options
context:
space:
mode:
authorYann Herklotz <git@yannherklotz.com>2020-07-24 10:28:15 +0100
committerYann Herklotz <git@yannherklotz.com>2020-07-24 10:28:15 +0100
commitb6a094c0e3b1b5bef06d932fc73f09aba88a4fda (patch)
treef7404722d3585c083e90f8d6b1379a65ddcd64ca /src/Compiler.v
parent5cf10a4c70763cbb95747b19ac35b57a9dee4dd5 (diff)
downloadvericert-b6a094c0e3b1b5bef06d932fc73f09aba88a4fda.tar.gz
vericert-b6a094c0e3b1b5bef06d932fc73f09aba88a4fda.zip
Remove check mpass
Diffstat (limited to 'src/Compiler.v')
-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