From b92c98dab28ab33143a57a8aca37028ff544cdd5 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Sun, 18 Dec 2016 17:06:35 +0100
Subject: [PATCH] Copy should be an implicit argument
---
theories/typing/type_context.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 9d354493..ca37fc22 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -83,7 +83,7 @@ Section type_context.
by iApply (Hincl with "LFT HE HL").
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].
Proof.
iIntros (???) "_ $ $ *". rewrite /tctx_interp !big_sepL_cons big_sepL_nil.
--
GitLab