diff options
| -rw-r--r-- | checker/check.mllib | 1 | ||||
| -rw-r--r-- | checker/values.ml | 2 | ||||
| -rw-r--r-- | clib/canary.ml | 28 | ||||
| -rw-r--r-- | clib/canary.mli | 27 | ||||
| -rw-r--r-- | clib/clib.mllib | 1 | ||||
| -rw-r--r-- | kernel/names.ml | 11 |
6 files changed, 5 insertions, 65 deletions
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 |