Skip to content
Snippets Groups Projects
Commit c44ce4c9 authored by Ralf Jung's avatar Ralf Jung
Browse files

make lc_supply Local

parent d48b71ab
Branches
No related tags found
No related merge requests found
......@@ -40,7 +40,7 @@ Notation "'£' n" := (lc n) (at level 1).
Users should not directly interface with this. *)
Local Definition lc_supply_def `{!lcGS Σ} (n : nat) : iProp Σ := own lcGS_name ( n).
Local Definition lc_supply_aux : seal (@lc_supply_def). Proof. by eexists. Qed.
Definition lc_supply := lc_supply_aux.(unseal).
Local Definition lc_supply := lc_supply_aux.(unseal).
Local Definition lc_supply_unseal :
@lc_supply = @lc_supply_def := lc_supply_aux.(seal_eq).
Global Arguments lc_supply {Σ _} n.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment