[gramlib] Remove legacy located exception wrapper in favor of standard infrastructure.

The old wrapper was basically unused, this PR also fixes backtraces in
some class of bugs such as https://github.com/coq/coq/issues/12695

1 files changed, 0 insertions, 14 deletions

diff --git a/gramlib/ploc.mli b/gramlib/ploc.mli
index 15a5a74455..4b865110c3 100644
--- a/gramlib/ploc.mli
+++ b/gramlib/ploc.mli
@@ -2,20 +2,6 @@
 (* ploc.mli,v *)
 (* Copyright (c) INRIA 2007-2017 *)
 
-(* located exceptions *)
-
-exception Exc of Loc.t * exn
-   (** [Ploc.Exc loc e] is an encapsulation of the exception [e] with
-       the input location [loc]. To be used to specify a location
-       for an error. This exception must not be raised by [raise] but
-       rather by [Ploc.raise] (see below), to prevent the risk of several
-       encapsulations of [Ploc.Exc]. *)
-
-val raise : Loc.t -> exn -> 'a
-   (** [Ploc.raise loc e], if [e] is already the exception [Ploc.Exc],
-       re-raise it (ignoring the new location [loc]), else raise the
-       exception [Ploc.Exc loc e]. *)
-
 val make_unlined : int * int -> Loc.t
    (** [Ploc.make_unlined] is like [Ploc.make] except that the line number
        is not provided (to be used e.g. when the line number is unknown. *)