diff options
Diffstat (limited to 'gramlib/ploc.mli')
| -rw-r--r-- | gramlib/ploc.mli | 14 |
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. *) |