From c1d0c0fefa6e341aa115591217d945dc366d1812 Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Mon, 26 Oct 2020 15:44:20 +0000
Subject: Add tbl_to_casestatement into extraction

---
 src/extraction/Extraction.v | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

(limited to 'src/extraction')

diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index d5cb9d7..879e752 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -22,7 +22,8 @@ From vericert Require
      Compiler
      RTLBlockgen
      RTLBlock
-     HTLSchedulegen.
+     HTLSchedulegen
+     HTLgen.
 
 From Coq Require DecidableClass.
 
@@ -180,6 +181,7 @@ Separate Extraction
          Verilog.module Value.uvalueToZ vericert.Compiler.transf_hls
          vericert.Compiler.transf_hls_temp
          RTLBlockgen.transl_program RTLBlock.successors_instr
+         HTLgen.tbl_to_case_expr
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
-- 
cgit