From be5f96ef61275c2d033f40a889f306a1e8219f31 Mon Sep 17 00:00:00 2001 From: Jacques-Henri Jourdan <jjourdan@mpi-sws.org> Date: Thu, 12 Jan 2017 13:43:37 +0100 Subject: [PATCH] Fix typo. --- 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 1c7c8c5c..5114941c 100644 --- a/theories/typing/unsafe/cell.v +++ b/theories/typing/unsafe/cell.v @@ -24,7 +24,7 @@ Section cell. (* TODO: non-expansiveness, proper wrt. eqtype *) - Global Instance cell_type : + Global Instance cell_copy : Copy ty → Copy (cell ty). Proof. intros ty Hcopy. split; first by intros; simpl; apply _. -- GitLab