Fix imports to remove warnings when compiling

1 files changed, 23 insertions, 18 deletions

diff --git a/src/hls/Veriloggen.v b/src/hls/Veriloggen.v
index a0be0fa..80c0669 100644
--- a/src/hls/Veriloggen.v
+++ b/src/hls/Veriloggen.v
@@ -16,10 +16,15 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  *)
 
-From compcert Require Import Maps.
-From compcert Require Errors.
-From compcert Require Import AST.
-From vericert Require Import Verilog HTL Vericertlib AssocMap ValueInt.
+Require Import compcert.common.AST.
+Require compcert.common.Errors.
+Require Import compcert.lib.Maps.
+
+Require Import vericert.common.Vericertlib.
+Require Import vericert.hls.AssocMap.
+Require Import vericert.hls.HTL.
+Require Import vericert.hls.ValueInt.
+Require Import vericert.hls.Verilog.
 
 Definition transl_list_fun (a : node * Verilog.stmnt) :=
   let (n, stmnt) := a in
@@ -41,23 +46,23 @@ Definition transl_module (m : HTL.module) : Verilog.module :=
   let case_el_ctrl := transl_list (PTree.elements m.(mod_controllogic)) in
   let case_el_data := transl_list (PTree.elements m.(mod_datapath)) in
   let body :=
-      Valways (Vposedge m.(mod_clk)) (Vcond (Vbinop Veq (Vvar m.(mod_reset)) (Vlit (ZToValue 1)))
-                                               (Vnonblock (Vvar m.(mod_st)) (Vlit (posToValue m.(mod_entrypoint))))
-                                               (Vcase (Vvar m.(mod_st)) case_el_ctrl (Some Vskip)))
-      :: Valways (Vposedge m.(mod_clk)) (Vcase (Vvar m.(mod_st)) case_el_data (Some Vskip))
+      Valways (Vposedge m.(HTL.mod_clk)) (Vcond (Vbinop Veq (Vvar m.(HTL.mod_reset)) (Vlit (ZToValue 1)))
+                                               (Vnonblock (Vvar m.(HTL.mod_st)) (Vlit (posToValue m.(HTL.mod_entrypoint))))
+                                               (Vcase (Vvar m.(HTL.mod_st)) case_el_ctrl (Some Vskip)))
+      :: Valways (Vposedge m.(HTL.mod_clk)) (Vcase (Vvar m.(HTL.mod_st)) case_el_data (Some Vskip))
       :: List.map Vdeclaration (arr_to_Vdeclarr (AssocMap.elements m.(mod_arrdecls))
                           ++ scl_to_Vdecl (AssocMap.elements m.(mod_scldecls))) in
-  Verilog.mkmodule m.(mod_start)
-                   m.(mod_reset)
-                   m.(mod_clk)
-                   m.(mod_finish)
-                   m.(mod_return)
-                   m.(mod_st)
-                   m.(mod_stk)
-                   m.(mod_stk_len)
-                   m.(mod_params)
+  Verilog.mkmodule m.(HTL.mod_start)
+                   m.(HTL.mod_reset)
+                   m.(HTL.mod_clk)
+                   m.(HTL.mod_finish)
+                   m.(HTL.mod_return)
+                   m.(HTL.mod_st)
+                   m.(HTL.mod_stk)
+                   m.(HTL.mod_stk_len)
+                   m.(HTL.mod_params)
                    body
-                   m.(mod_entrypoint).
+                   m.(HTL.mod_entrypoint).
 
 Definition transl_fundef := transf_fundef transl_module.