Commit ab4583c1 authored by Glen Mével's avatar Glen Mével

Fix comments.

parent a11f6dae
...@@ -188,7 +188,7 @@ End TickSpec. ...@@ -188,7 +188,7 @@ End TickSpec.
(* (*
* Operation semantics of `tick` * Operational semantics of `tick`
*) *)
Section Tick_lemmas. Section Tick_lemmas.
......
...@@ -332,7 +332,7 @@ Section Soundness. ...@@ -332,7 +332,7 @@ Section Soundness.
(* allocate the ghost state associated with : *) (* allocate the ghost state associated with : *)
iMod (auth_nat_alloc 0) as (γ1) "[Hγ1● _]". iMod (auth_nat_alloc 0) as (γ1) "[Hγ1● _]".
iMod (auth_mnat_alloc 0) as (γ2) "[Hγ2● _]". iMod (auth_mnat_alloc 0) as (γ2) "[Hγ2● _]".
(* packing all those bits, build the heap instance necessary to use time credits: *) (* packing all those bits, build the heap instance necessary to use time receipts: *)
pose (Build_timeReceiptHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ h)) _ _ _ γ1 γ2) pose (Build_timeReceiptHeapG Σ (HeapG Σ _ (GenHeapG _ _ Σ _ _ _ h)) _ _ _ γ1 γ2)
as HtrHeapG. as HtrHeapG.
(* create the invariant: *) (* create the invariant: *)
......
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