Skip to content
Snippets Groups Projects
Commit 09096359 authored by Felipe Lisboa's avatar Felipe Lisboa
Browse files

Fix: Default_arbitrate definition does not need a Program command

parent 83c51d8a
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
framework/DDR3/ImplementationInterface.v
+ 1
− 1
View file @ 09096359
...@@ -27,7 +27,7 @@ Section ImplementationInterface. ...@@ -27,7 +27,7 @@ Section ImplementationInterface.
Next : Requests_t -> State_t -> State_t * (Command_kind_t * Request_t); 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 let R := Arrival_at t in
match t with match t with
| 0 => mkArbiterState [::] t (Init R) | 0 => mkArbiterState [::] t (Init R)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment