Getting rid of LtacLocated exception transformer.

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

2 files changed, 9 insertions, 10 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 8da15e8da7..84149beadb 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -195,7 +195,6 @@ let e_possible_resolve db_list local_db gl =
 
 let rec catchable = function
   | Refiner.FailError _ -> true
-  | Proof_type.LtacLocated (_, _, e) -> catchable e
   | e -> Logic.catchable_exception e
 
 let nb_empty_evars s =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 7ee5a67196..6e2aceaff9 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -71,19 +71,21 @@ let dloc = Loc.ghost
 let catch_error call_trace tac g =
   try tac g with e when Errors.noncritical e ->
   let e = Errors.push e in
-  let inner_trace,loc,e = match e with
-  | LtacLocated (inner_trace,loc,e) -> inner_trace,loc,e
-  | e ->
+  let inner_trace,loc,e = match Exninfo.get e ltac_trace_info with
+  | Some (inner_trace,loc) -> inner_trace,loc,e
+  | None ->
     let loc = match Loc.get_loc e with
     | None -> Loc.ghost
     | Some loc -> loc
     in
     [], loc, e
   in
-  if List.is_empty call_trace & List.is_empty inner_trace then raise e
+  if List.is_empty call_trace && List.is_empty inner_trace then raise e
   else begin
-    assert (Errors.noncritical e); (* preserved invariant about LtacLocated *)
-    raise (LtacLocated(inner_trace@call_trace,loc,e))
+    assert (Errors.noncritical e); (* preserved invariant *)
+    let new_trace = inner_trace @ call_trace in
+    let located_exc = Exninfo.add e ltac_trace_info (new_trace, loc) in
+    raise located_exc
   end
 
 (* Signature for interpretation: val_interp and interpretation functions *)
@@ -1215,12 +1217,10 @@ and eval_with_fail ist is_lazy goal tac =
     | a -> a)
   with
     (** FIXME: Should we add [Errors.push]? *)
-    | FailError (0,s) | LtacLocated (_,_,FailError (0,s)) ->
+    | FailError (0,s) ->
 	raise (Eval_fail (Lazy.force s))
     | FailError (lvl,s) as e ->
         raise (Exninfo.copy e (FailError (lvl - 1, s)))
-    | LtacLocated (s'',loc,FailError (lvl,s')) ->
-	raise (LtacLocated (s'',loc,FailError (lvl - 1, s')))
 
 (* Interprets the clauses of a recursive LetIn *)
 and interp_letrec ist gl llc u =