diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-19 12:49:21 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2018-06-19 12:49:21 +0200 |
commit | 017d5133d8ec7339bf8170c98822638a58b66b14 (patch) | |
tree | d1185c09a96e9b9ba5ed4074c1a597682af5a9c1 /clib/canary.ml | |
parent | 981864d47efca1d42f43dc5b7c5439638a86f315 (diff) | |
parent | 6483605e9bea9dfb823934f4f8c8e89bd7977d4c (diff) |
Merge PR #7841: Remove Canary
Diffstat (limited to 'clib/canary.ml')
-rw-r--r-- | clib/canary.ml | 28 |
1 files changed, 0 insertions, 28 deletions
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 |