From 6483605e9bea9dfb823934f4f8c8e89bd7977d4c Mon Sep 17 00:00:00 2001
From: whitequark <whitequark@whitequark.org>
Date: Sat, 16 Jun 2018 12:31:22 +0000
Subject: Remove Canary.

This eliminates 3 uses of Obj from TCB.
---
 clib/canary.ml  | 28 ----------------------------
 clib/canary.mli | 27 ---------------------------
 clib/clib.mllib |  1 -
 3 files changed, 56 deletions(-)
 delete mode 100644 clib/canary.ml
 delete mode 100644 clib/canary.mli

(limited to 'clib')

diff --git a/clib/canary.ml b/clib/canary.ml
deleted file mode 100644
index b8b79ed7f..000000000
--- a/clib/canary.ml
+++ /dev/null
@@ -1,28 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-type t = Obj.t
-
-let obj = Obj.new_block Obj.closure_tag 0
-  (** This is an empty closure block. In the current implementation, it is
-      sufficient to allow marshalling but forbid equality. Sadly still allows
-      hash. *)
-  (** FIXME : use custom blocks somehow. *)
-
-module type Obj = sig type t end
-
-module Make(M : Obj) =
-struct
-  type canary = t
-  type t = (canary * M.t)
-
-  let prj (_, x) = x
-  let inj x = (obj, x)
-end
diff --git a/clib/canary.mli b/clib/canary.mli
deleted file mode 100644
index d993eabcf..000000000
--- a/clib/canary.mli
+++ /dev/null
@@ -1,27 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
-(* <O___,, *       (see CREDITS file for the list of authors)           *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-type t
-(** Type of canaries. Canaries are used to ensure that an object does not use
-    generic operations. *)
-
-val obj : t
-(** Canary. In the current implementation, this object is marshallable,
-    forbids generic comparison but still allows generic hashes. *)
-
-module type Obj = sig type t end
-
-module Make(M : Obj) :
-sig
-  type t
-  val prj : t -> M.t
-  val inj : M.t -> t
-end
-(** Adds a canary to any type. *)
diff --git a/clib/clib.mllib b/clib/clib.mllib
index c9b4d72fc..afece4074 100644
--- a/clib/clib.mllib
+++ b/clib/clib.mllib
@@ -1,4 +1,3 @@
-Canary
 CObj
 CEphemeron
 
-- 
cgit v1.2.3