Commit a45346ba authored by Hai Dang's avatar Hai Dang
Browse files

Remove unnecessary Program

parent 973d7a72
......@@ -72,7 +72,7 @@ Proof using All.
- by iIntros "$".
Qed.
Program Definition exchanger_impl_from_piggyback :
Definition exchanger_impl_from_piggyback :
exchanger_spec Σ := {|
spec_graph.ExchangerLocal := ExchangerLocal' ;
spec_graph.ExchangerInv := ExchangerInv' ;
......
......@@ -2856,7 +2856,7 @@ Proof.
Qed.
End proof.
Program Definition hwqueue_impl (sz : positive) (b : bool)
Definition hwqueue_impl (sz : positive) (b : bool)
Σ `{!noprolG Σ, !hwqG Σ, !atomicG Σ} :
weak_queue_spec Σ := {|
spec_graph.QueueInv_Objective := QueueInv_objective;
......
......@@ -3480,7 +3480,7 @@ Qed.
End proof.
Program Definition msqueue_impl_strong
Definition msqueue_impl_strong
Σ `{!noprolG Σ, !msqueueG Σ, !atomicG Σ} :
strong_queue_spec Σ := {|
spec_graph.QueueInv_Objective := QueueInv_objective;
......
......@@ -2660,7 +2660,7 @@ Proof.
Qed.
End proof.
Program Definition elimination_stack_impl Σ
Definition elimination_stack_impl Σ
`{!noprolG Σ, !inG Σ (graphR sevent), !inG Σ (graphR xchg_event),
!ro_ptstoG Σ, !inG Σ (mono_listR (leibnizO (event_id + event_id)))}
(stk : a_stack_spec Σ) (ex : exchanger_piggyback_spec Σ)
......
......@@ -2149,7 +2149,7 @@ Proof.
Qed.
End proof.
Program Definition treiber_stack_impl Σ
Definition treiber_stack_impl Σ
`{!noprolG Σ, !tstackG Σ, !atomicG Σ} : a_stack_spec Σ := {|
spec_graph.StackInv_Objective := StackInv_objective ;
spec_graph.StackInv_Fractional := StackInv_fractional ;
......
Markdown is supported
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