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

Minor cleanup

parent d249c8f3
......@@ -373,7 +373,7 @@ Record ExtendedStackConsistent G : Prop := mkExtendedStackConsistent {
exstk_cons_dview_pop : (* pop is acquiring *) stack_pop_acquiring G ;
(* (1)-(7) Stack spec from POPL'19 Library Correctness paper *)
exstk_cons_basic : StackConsistent G ;
exstk_cons_basic :> StackConsistent G ;
(* The last one is our strengthening that holds for stronger implementation. *)
exstk_cons_LIFO_b :
......@@ -412,7 +412,6 @@ Program Definition extended_to_basic_stack_spec
StackInv_Fractional := stk.(StackInv_Fractional) ;
StackInv_AsFractional := stk.(StackInv_AsFractional) ;
(* StackInv_StackConsistent := ∀ γg s q G, StackInv γg s q G ⊢ ⌜ StackConsistent G ⌝ ; *)
StackInv_graph_master_acc := stk.(StackInv_graph_master_acc) ;
StackInv_graph_snap := stk.(StackInv_graph_snap) ;
StackInv_agree := stk.(StackInv_agree) ;
......
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