From 4139d0f8772d20d2836be2ab34a18b5ce580590b Mon Sep 17 00:00:00 2001
From: Michalis Pardalos <m.pardalos@gmail.com>
Date: Tue, 31 Aug 2021 13:05:20 +0100
Subject: Get Renaming compiling with RAM inference

---
 src/hls/ApplyExternctrl.v | 14 --------------
 1 file changed, 14 deletions(-)

(limited to 'src/hls/ApplyExternctrl.v')

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);
-- 
cgit