From 5877d6c92846f0c8562e2b3a6e4cfd79a04a8c5d Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Thu, 20 Sep 2018 23:54:01 +0200
Subject: [PATCH] Coq bug 5326 is not solved. We have better notations.
---
theories/typing/lib/mutex/mutexguard.v | 8 ++++----
theories/typing/lib/refcell/ref_code.v | 4 +---
theories/typing/lib/refcell/refmut_code.v | 9 ++++-----
3 files changed, 9 insertions(+), 12 deletions(-)
diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index be34421c..3136bd97 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -192,8 +192,8 @@ Section code.
delete [ #1; "g"];; return: ["r"].
Lemma mutexguard_derefmut_type ty `{!TyWf ty} :
- typed_val mutexguard_derefmut (fn (fun '(α, β) =>
- FP_wf ∅ [# &uniq{α}(mutexguard β ty)]%T (&uniq{α}ty)%T)).
+ typed_val mutexguard_derefmut
+ (fn(∀ '(α, β), ∅; &uniq{α}(mutexguard β ty)) → &uniq{α}ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ϝ ret arg). inv_vec arg=>g. simpl_subst.
@@ -234,8 +234,8 @@ Section code.
Definition mutexguard_deref : val := mutexguard_derefmut.
Lemma mutexguard_deref_type ty `{!TyWf ty} :
- typed_val mutexguard_derefmut (fn (fun '(α, β) =>
- FP_wf ∅ [# &shr{α}(mutexguard β ty)]%T (&shr{α}ty)%T)).
+ typed_val mutexguard_derefmut
+ (fn(∀ '(α, β), ∅; &shr{α}(mutexguard β ty)) → &shr{α}ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ϝ ret arg). inv_vec arg=>g. simpl_subst.
diff --git a/theories/typing/lib/refcell/ref_code.v b/theories/typing/lib/refcell/ref_code.v
index 95ee3e02..84f92f9e 100644
--- a/theories/typing/lib/refcell/ref_code.v
+++ b/theories/typing/lib/refcell/ref_code.v
@@ -45,8 +45,6 @@ Section ref_functions.
letalloc: "r" <-{2} !"x'" in
delete [ #1; "x"];; return: ["r"].
- (* FIXME : using λ instead of fun triggers an anomaly.
- See: https://coq.inria.fr/bugs/show_bug.cgi?id=5326 *)
Lemma ref_clone_type ty `{!TyWf ty} :
typed_val ref_clone (fn(∀ '(α, β), ∅; &shr{α}(ref β ty)) → ref β ty).
@@ -110,7 +108,7 @@ Section ref_functions.
Lemma ref_deref_type ty `{!TyWf ty} :
typed_val ref_deref
- (fn (fun '(α, β) => FP_wf ∅ [# &shr{α}(ref β ty)]%T (&shr{α}ty)%T)).
+ (fn(∀ '(α, β), ∅; &shr{α}(ref β ty)) → &shr{α}ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
diff --git a/theories/typing/lib/refcell/refmut_code.v b/theories/typing/lib/refcell/refmut_code.v
index 82fa6c8d..89c81f6b 100644
--- a/theories/typing/lib/refcell/refmut_code.v
+++ b/theories/typing/lib/refcell/refmut_code.v
@@ -19,8 +19,7 @@ Section refmut_functions.
delete [ #1; "x"];; return: ["r"].
Lemma refmut_deref_type ty `{!TyWf ty} :
- typed_val refmut_deref (fn (fun '(α, β) =>
- FP_wf ∅ [# &shr{α}(refmut β ty)]%T (&shr{α}ty))).
+ typed_val refmut_deref (fn(∀ '(α, β), ∅; &shr{α}(refmut β ty)) → &shr{α}ty).
Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
@@ -57,9 +56,9 @@ Section refmut_functions.
Definition refmut_derefmut : val := refmut_deref.
Lemma refmut_derefmut_type ty `{!TyWf ty} :
- typed_val refmut_derefmut (fn (fun '(α, β) =>
- FP_wf ∅ [# &uniq{α}(refmut β ty)]%T (&uniq{α}ty)%T)).
- Proof.
+ typed_val refmut_derefmut
+ (fn(∀ '(α, β), ∅; &uniq{α}(refmut β ty)) → &uniq{α}ty).
+ Proof.
intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
iIntros ([α β] ϝ ret arg). inv_vec arg=>x. simpl_subst.
iApply type_deref; [solve_typing..|]. iIntros (x').
--
GitLab