1 files changed, 0 insertions, 104 deletions
diff --git a/lib/exninfo.ml b/lib/exninfo.ml
deleted file mode 100644
index d049dc6c..00000000
--- a/lib/exninfo.ml
+++ /dev/null
@@ -1,104 +0,0 @@
-(***********************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
-(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
-(*   \VV/  *************************************************************)
-(*    //   *      This file is distributed under the terms of the      *)
-(*         *       GNU Lesser General Public License Version 2.1       *)
-(***********************************************************************)
-
-(** Enriched exceptions have an additional field at the end of their usual data
-    containing a pair composed of the distinguishing [token] and the backtrace
-    information. We discriminate the token by pointer equality. *)
-
-module Store = Store.Make(struct end)
-
-type 'a t = 'a Store.field
-
-type info = Store.t
-
-type iexn = exn * info
-
-let make = Store.field
-let add = Store.set
-let get = Store.get
-let null = Store.empty
-
-exception Unique
-
-let dummy = (Unique, Store.empty)
-
-let current : (int * iexn) list ref = ref []
-(** List associating to each thread id the latest exception raised by an
-    instrumented raise (i.e. {!raise} from this module). It is shared between
-    threads, so we must take care of this when modifying it.
-
-    Invariants: all index keys are unique in the list.
-*)
-
-let lock = Mutex.create ()
-
-let rec remove_assoc (i : int) = function
-| [] -> []
-| (j, v) :: rem as l ->
-  if i = j then rem
-  else
-    let ans = remove_assoc i rem in
-    if rem == ans then l
-    else (j, v) :: ans
-
-let rec find_and_remove_assoc (i : int) = function
-| [] -> dummy, []
-| (j, v) :: rem as l ->
-  if i = j then (v, rem)
-  else
-    let (r, ans) = find_and_remove_assoc i rem in
-    if rem == ans then (r, l)
-    else (r, (j, v) :: ans)
-
-let iraise e =
-  let () = Mutex.lock lock in
-  let id = Thread.id (Thread.self ()) in
-  let () = current := (id, e) :: remove_assoc id !current in
-  let () = Mutex.unlock lock in
-  raise (fst e)
-
-let raise ?info e = match info with
-| None ->
-  let () = Mutex.lock lock in
-  let id = Thread.id (Thread.self ()) in
-  let () = current := remove_assoc id !current in
-  let () = Mutex.unlock lock in
-  raise e
-| Some i ->
-  let () = Mutex.lock lock in
-  let id = Thread.id (Thread.self ()) in
-  let () = current := (id, (e, i)) :: remove_assoc id !current in
-  let () = Mutex.unlock lock in
-  raise e
-
-let find_and_remove () =
-  let () = Mutex.lock lock in
-  let id = Thread.id (Thread.self ()) in
-  let (v, l) = find_and_remove_assoc id !current in
-  let () = current := l in
-  let () = Mutex.unlock lock in
-  v
-
-let info e =
-  let (src, data) = find_and_remove () in
-  if src == e then
-    (** Slightly unsound, some exceptions may not be unique up to pointer
-        equality. Though, it should be quite exceptional to be in a situation
-        where the following holds:
-
-        1. An argument-free exception is raised through the enriched {!raise};
-        2. It is not captured by any enriched with-clause (which would reset
-            the current data);
-        3. The same exception is raised through the standard raise, accessing
-            the wrong data.
-    . *)
-    data
-  else
-    (** Mismatch: the raised exception is not the one stored, either because the
-        previous raise was not instrumented, or because something went wrong. *)
-    Store.empty