From 5361e9fa3119a374f0dcbadce2faf6ec3d7f5dcd Mon Sep 17 00:00:00 2001
From: Florian Brandner <florian.brandner@telecom-paris.fr>
Date: Fri, 7 May 2021 09:28:23 +0200
Subject: [PATCH] fix type error
---
coq/FIFO.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/coq/FIFO.v b/coq/FIFO.v
index 05f3c79..e478a4f 100644
--- a/coq/FIFO.v
+++ b/coq/FIFO.v
@@ -291,7 +291,7 @@ Section FIFO.
Program Definition FIFO_arbitrate :=
let State := FIFO_trace Requests in
- mkTrace State.(Cmds) State.(Time) _ (FIFO_trace_time_ok Requests) _ (FIFO_trace_T_RC_ok Requests).
+ mkTrace State.(Cmds) State.(Time) _ (FIFO_trace_time_ok Requests) _ (FIFO_trace_T_RC_ok Requests) _.
Admit Obligations.
(*
--
GitLab