From 6d40a9e8f57a91afc1f292dbb0f72800da2e0d21 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 17 Jan 2017 10:48:54 +0100
Subject: [PATCH] don't register instance twice
---
theories/typing/function.v | 2 +-
1 file changed, 1 insertion(+), 1 deletion(-)
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 5b02c5a5..9030e408 100644
--- a/theories/typing/function.v
+++ b/theories/typing/function.v
@@ -24,7 +24,7 @@ Section fn.
Global Instance fn_send E tys ty : Send (fn E tys ty).
Proof. iIntros (tid1 tid2 vl). done. Qed.
- Instance fn_contractive n' E :
+ Lemma fn_contractive n' E :
Proper (pointwise_relation A (dist_later n') ==>
pointwise_relation A (dist_later n') ==> dist n') (fn E).
Proof.
--
GitLab