From 22cd25ab9aa3c95003e5728397f0864c613dde58 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 8 Feb 2017 13:55:12 +0100
Subject: [PATCH] Cell::get_mut does not need the type to be copy

---
 theories/typing/unsafe/cell.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/typing/unsafe/cell.v b/theories/typing/unsafe/cell.v
index 878c6ba0..687b41cc 100644
--- a/theories/typing/unsafe/cell.v
+++ b/theories/typing/unsafe/cell.v
@@ -103,7 +103,7 @@ Section typing.
   Definition cell_get_mut : val :=
     funrec: <> ["x"] := "return" ["x"].
 
-  Lemma cell_get_mut_type `(!Copy ty) :
+  Lemma cell_get_mut_type ty :
     typed_instruction_ty [] [] [] cell_get_mut
       (fn (λ α, [☀α])%EL (λ α, [# &uniq{α} (cell ty)])%T (λ α, &uniq{α} ty)%T).
   Proof.
-- 
GitLab