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.
---
 checker/check.mllib |  1 -
 checker/values.ml   |  2 +-
 clib/canary.ml      | 28 ----------------------------
 clib/canary.mli     | 27 ---------------------------
 clib/clib.mllib     |  1 -
 kernel/names.ml     | 11 ++++-------
 6 files changed, 5 insertions(+), 65 deletions(-)
 delete mode 100644 clib/canary.ml
 delete mode 100644 clib/canary.mli

diff --git a/checker/check.mllib b/checker/check.mllib
index f79ba66e3..139fa765b 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -3,7 +3,6 @@ Coq_config
 Analyze
 Hook
 Terminal
-Canary
 Hashset
 Hashcons
 CSet
diff --git a/checker/values.ml b/checker/values.ml
index 67032bd1b..38032a6ca 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -91,7 +91,7 @@ let rec v_mp = Sum("module_path",0,
   [|[|v_dp|];
     [|v_uid|];
     [|v_mp;v_id|]|])
-let v_kn = v_tuple "kernel_name" [|Any;v_mp;v_dp;v_id;Int|]
+let v_kn = v_tuple "kernel_name" [|v_mp;v_dp;v_id;Int|]
 let v_cst = v_sum "cst|mind" 0 [|[|v_kn|];[|v_kn;v_kn|]|]
 let v_ind = v_tuple "inductive" [|v_cst;Int|]
 let v_cons = v_tuple "constructor" [|v_ind;Int|]
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
 
diff --git a/kernel/names.ml b/kernel/names.ml
index 597061278..1d2a7c4ce 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -17,7 +17,7 @@
    the module system, Aug 2002 *)
 (* Abstraction over the type of constant for module inlining by Claudio
    Sacerdoti, Nov 2004 *)
-(* Miscellaneous features or improvements by Hugo Herbelin, 
+(* Miscellaneous features or improvements by Hugo Herbelin,
    Élie Soubiran, ... *)
 
 open Pp
@@ -364,7 +364,6 @@ module MPmap = CMap.Make(ModPath)
 module KerName = struct
 
   type t = {
-    canary : Canary.t;
     modpath : ModPath.t;
     dirpath : DirPath.t;
     knlabel : Label.t;
@@ -372,16 +371,14 @@ module KerName = struct
     (** Lazily computed hash. If unset, it is set to negative values. *)
   }
 
-  let canary = Canary.obj
-
   type kernel_name = t
 
   let make modpath dirpath knlabel =
-    { modpath; dirpath; knlabel; refhash = -1; canary; }
+    { modpath; dirpath; knlabel; refhash = -1; }
   let repr kn = (kn.modpath, kn.dirpath, kn.knlabel)
 
   let make2 modpath knlabel =
-    { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; canary; }
+    { modpath; dirpath = DirPath.empty; knlabel; refhash = -1; }
 
   let modpath kn = kn.modpath
   let label kn = kn.knlabel
@@ -437,7 +434,7 @@ module KerName = struct
         * (string -> string)
     let hashcons (hmod,hdir,hstr) kn =
       let { modpath = mp; dirpath = dp; knlabel = l; refhash; } = kn in
-      { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; canary; }
+      { modpath = hmod mp; dirpath = hdir dp; knlabel = hstr l; refhash; }
     let eq kn1 kn2 =
       kn1.modpath == kn2.modpath && kn1.dirpath == kn2.dirpath &&
         kn1.knlabel == kn2.knlabel
-- 
cgit v1.2.3