Get Renaming compiling with RAM inference

1 files changed, 0 insertions, 14 deletions

diff --git a/src/hls/ApplyExternctrl.v b/src/hls/ApplyExternctrl.v
index ef056cf..bd48adb 100644
--- a/src/hls/ApplyExternctrl.v
+++ b/src/hls/ApplyExternctrl.v
@@ -142,20 +142,6 @@ Section APPLY_EXTERNCTRL.
     do l <- xassocmap_apply_externctrl (AssocMap.elements regmap);
     OK (AssocMap_Properties.of_list l).
 
-  Definition option_ram_wf (clk : reg) (mr : option HTL.ram) :
-    option (forall r' : ram, mr = Some r' -> (clk < ram_addr r')%positive).
-    refine (
-    match mr with
-    | Some r =>
-      match (plt clk (ram_addr r)) with
-      | left LE => Some _
-      | _ => None
-      end
-    | None => None
-    end).
-    crush.
-  Defined.
-
   Definition module_apply_externctrl : res HTL.module :=
     do mod_start' <- reg_apply_externctrl (HTL.mod_start m);
     do mod_reset' <- reg_apply_externctrl (HTL.mod_reset m);