Removing Exc_located and using the new exception enrichement

mechanism to retrieve the same information.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16215 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 11 insertions, 5 deletions

diff --git a/lib/loc.mli b/lib/loc.mli
index c712cddd9..a0b99c689 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -10,8 +10,6 @@
 
 type t
 
-exception Exc_located of t * exn
-
 type 'a located = t * 'a
 (** Embed a location in a type *)
 
@@ -37,12 +35,20 @@ val is_ghost : t -> bool
 
 val merge : t -> t -> t
 
-val raise : t -> exn -> 'a
-(** Raise a located exception *)
-
 val represent : t -> (string * int * int * int * int)
 (** Return the arguments given in [create] *)
 
+(** {5 Located exceptions} *)
+
+val add_loc : exn -> t -> exn
+(** Adding location to an exception *)
+
+val get_loc : exn -> t option
+(** Retrieving the optional location of an exception *)
+
+val raise : t -> exn -> 'a
+(** [raise loc e] is the same as [Pervasives.raise (add_loc e loc)]. *)
+
 (** {5 Location utilities} *)
 
 val located_fold_left : ('a -> 'b -> 'a) -> 'a -> 'b located -> 'a