From c6eb1f473b65480f52fec446b6d4b8467b32ef90 Mon Sep 17 00:00:00 2001
From: Florian Brandner <florian.brandner@telecom-paris.fr>
Date: Fri, 7 May 2021 12:59:51 +0200
Subject: [PATCH] fix type error (correctly)
---
coq/FIFO.v | 9 +++------
1 file changed, 3 insertions(+), 6 deletions(-)
diff --git a/coq/FIFO.v b/coq/FIFO.v
index e478a4f..4bd99a7 100644
--- a/coq/FIFO.v
+++ b/coq/FIFO.v
@@ -291,15 +291,12 @@ 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) _.
- Admit Obligations.
-
- (*
+ mkTrace State.(Cmds) State.(Time) _ (FIFO_trace_time_ok Requests) (FIFO_trace_Cmds_PRE_ok Requests) (FIFO_trace_T_RC_ok Requests) (FIFO_trace_T_RP_ok Requests).
Next Obligation.
induction Requests.
- - auto.
+ - auto.
- by apply (FIFO_trace_uniq a) in IHl.
- *)
+ Qed.
Lemma FIFO_trace_Req_handled Reqs:
forall req, req \in Reqs ->
--
GitLab