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 | |
| parent | 981864d47efca1d42f43dc5b7c5439638a86f315 (diff) | |
| parent | 6483605e9bea9dfb823934f4f8c8e89bd7977d4c (diff) | |
Merge PR #7841: Remove Canary
Diffstat (limited to 'clib')
| -rw-r--r-- | clib/canary.ml | 28 | ||||
| -rw-r--r-- | clib/canary.mli | 27 | ||||
| -rw-r--r-- | clib/clib.mllib | 1 |
3 files changed, 0 insertions, 56 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 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 |