From f4b638e7b82c7fa728104aa37e9e70a91ab62fd3 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Sat, 25 Feb 2017 17:36:14 +0100
Subject: [PATCH] Cosmetic changes in refcell.

---
 theories/typing/unsafe/refcell/refmut_code.v | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

diff --git a/theories/typing/unsafe/refcell/refmut_code.v b/theories/typing/unsafe/refcell/refmut_code.v
index 0214e24d..14214350 100644
--- a/theories/typing/unsafe/refcell/refmut_code.v
+++ b/theories/typing/unsafe/refcell/refmut_code.v
@@ -10,8 +10,6 @@ Set Default Proof Using "Type".
 Section refmut_functions.
   Context `{typeG Σ, refcellG Σ}.
 
-  (* TODO : map, when we will have a nice story about closures. *)
-
   (* Turning a refmut into a shared borrow. *)
   Definition refmut_deref : val :=
     funrec: <> ["x"] :=
@@ -63,7 +61,7 @@ Section refmut_functions.
       delete [ #1; "x"];; "return" ["r"].
 
   Lemma refmut_derefmut_type ty :
-    typed_instruction_ty [] [] [] refmut_deref
+    typed_instruction_ty [] [] [] refmut_derefmut
       (fn (fun '(α, β) => [☀α; ☀β; α ⊑ β])%EL
           (fun '(α, β) => [# &uniq{α}(refmut β ty)]%T)
           (fun '(α, β) => &uniq{α}ty)%T).
-- 
GitLab