Coq bug 5326 is not solved. We have better notations.

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.

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.

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').