From 09096359738d84d035a96a11aae442f85754b4ac Mon Sep 17 00:00:00 2001
From: Felipe Lisboa <lisboafelipe5@gmail.com>
Date: Fri, 2 Sep 2022 12:21:09 +0200
Subject: [PATCH] Fix: Default_arbitrate definition does not need a Program
command
---
framework/DDR3/ImplementationInterface.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/framework/DDR3/ImplementationInterface.v b/framework/DDR3/ImplementationInterface.v
index 0392b5a..4281193 100644
--- a/framework/DDR3/ImplementationInterface.v
+++ b/framework/DDR3/ImplementationInterface.v
@@ -27,7 +27,7 @@ Section ImplementationInterface.
Next : Requests_t -> State_t -> State_t * (Command_kind_t * Request_t);
}.
- Program Fixpoint Default_arbitrate {AF : Arrival_function_t} {IM : Implementation_t} t {struct t}: Arbiter_state_t :=
+ Fixpoint Default_arbitrate {AF : Arrival_function_t} {IM : Implementation_t} t {struct t}: Arbiter_state_t :=
let R := Arrival_at t in
match t with
| 0 => mkArbiterState [::] t (Init R)
--
GitLab