Skip to content
Snippets Groups Projects
Commit c6eb1f47 authored by Florian Brandner's avatar Florian Brandner
Browse files

fix type error (correctly)

parent 5361e9fa
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 3 additions and 6 deletions
coq/FIFO.v
+ 3
− 6
View file @ c6eb1f47
...@@ -291,15 +291,12 @@ Section FIFO. ...@@ -291,15 +291,12 @@ Section FIFO.
Program Definition FIFO_arbitrate := Program Definition FIFO_arbitrate :=
let State := FIFO_trace Requests in 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_Cmds_PRE_ok Requests) (FIFO_trace_T_RC_ok Requests) (FIFO_trace_T_RP_ok Requests).
Admit Obligations.
(*
Next Obligation. Next Obligation.
induction Requests. induction Requests.
- auto. - auto.
- by apply (FIFO_trace_uniq a) in IHl. - by apply (FIFO_trace_uniq a) in IHl.
*) Qed.
Lemma FIFO_trace_Req_handled Reqs: Lemma FIFO_trace_Req_handled Reqs:
forall req, req \in Reqs -> forall req, req \in Reqs ->
......
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