From 1fcdf60bb6b632c64609708e83453558a4bbea6b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 16 Jan 2017 22:26:47 +0100
Subject: [PATCH] moar parallel function.v
---
theories/typing/function.v | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/theories/typing/function.v b/theories/typing/function.v
index 6e62148f..5b02c5a5 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.
- Global Instance fn_contractive n' E :
+ Instance fn_contractive n' E :
Proper (pointwise_relation A (dist_later n') ==>
pointwise_relation A (dist_later n') ==> dist n') (fn E).
Proof.
@@ -50,6 +50,7 @@ Section fn.
* iIntros "H". by iApply "H".
* iIntros "H * #EQ". by iDestruct "EQ" as %[=->].
Qed.
+ Global Existing Instance fn_contractive.
Global Instance fn_ne n' E :
Proper (pointwise_relation A (dist n') ==>
--
GitLab