From 6cb38f39f5609651691419c6a299b09695a4623c Mon Sep 17 00:00:00 2001
From: Yann Herklotz <git@yannherklotz.com>
Date: Sun, 30 Aug 2020 16:06:25 +0100
Subject: Continue on Partitioning algorithm

---
 src/extraction/Extraction.v | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'src/extraction')

diff --git a/src/extraction/Extraction.v b/src/extraction/Extraction.v
index e6ee512..9755125 100644
--- a/src/extraction/Extraction.v
+++ b/src/extraction/Extraction.v
@@ -20,7 +20,8 @@ From vericert Require
      Verilog
      Value
      Compiler
-     RTLBlockgen.
+     RTLBlockgen
+     RTLBlock.
 
 From Coq Require DecidableClass.
 
@@ -174,7 +175,7 @@ Set Extraction AccessOpaque.
 Cd "src/extraction".
 Separate Extraction
          Verilog.module Value.uvalueToZ vericert.Compiler.transf_hls
-         RTLBlockgen.transl_program
+         RTLBlockgen.transl_program RTLBlock.successors_instr
 
    Compiler.transf_c_program Compiler.transf_cminor_program
    Cexec.do_initial_state Cexec.do_step Cexec.at_final_state
-- 
cgit