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

Copy should be an implicit argument

parent d3414ad2
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
theories/typing/type_context.v
+ 1
− 1
View file @ b92c98da
...@@ -83,7 +83,7 @@ Section type_context. ...@@ -83,7 +83,7 @@ Section type_context.
by iApply (Hincl with "LFT HE HL"). by iApply (Hincl with "LFT HE HL").
Qed. Qed.
Lemma copy_tctx_incl E L p `(!Copy ty) : Lemma copy_tctx_incl E L p `{!Copy ty} :
tctx_incl E L [TCtx_hasty p ty] [TCtx_hasty p ty; TCtx_hasty p ty]. tctx_incl E L [TCtx_hasty p ty] [TCtx_hasty p ty; TCtx_hasty p ty].
Proof. Proof.
iIntros (???) "_ $ $ *". rewrite /tctx_interp !big_sepL_cons big_sepL_nil. iIntros (???) "_ $ $ *". rewrite /tctx_interp !big_sepL_cons big_sepL_nil.
......
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