From 830f16e9506957198d10d6e46b502102ed38aa8d Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 13 May 2017 10:59:00 +0200
Subject: [PATCH] Fix FIXME.
The hypothesis was introduced into the pure context, because it is
convertible to True. IMHO, the ** introduction pattern is not something
that should be used often, so, I replace it.
---
theories/typing/lib/spawn.v | 9 ++-------
1 file changed, 2 insertions(+), 7 deletions(-)
diff --git a/theories/typing/lib/spawn.v b/theories/typing/lib/spawn.v
index 6e66ef5c..9fe858a5 100644
--- a/theories/typing/lib/spawn.v
+++ b/theories/typing/lib/spawn.v
@@ -65,13 +65,8 @@ Section join_handle.
unfold join_inv. iApply @send_change_tid. done.
Qed.
- Global Instance join_handle_sync ty :
- Sync (join_handle ty).
- Proof.
- iIntros (????) "**". (* FIXME: Why did it throw away the assumption we should have gotten? *)
- done.
- Qed.
-
+ Global Instance join_handle_sync ty : Sync (join_handle ty).
+ Proof. iIntros (????) "_ //". Qed.
End join_handle.
Section spawn.
--
GitLab