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

4 files changed, 18 insertions, 14 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index c70351caaf..329be18eb1 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
-  | Loc.Exc_located (_, e) -> catchable e
   | Proof_type.LtacLocated (_, _, e) -> catchable e
   | e -> Logic.catchable_exception e
 
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index f802788d48..7a8cccc6d7 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -596,9 +596,10 @@ let hResolve id c occ t gl =
   let rec resolve_hole t_hole =
     try 
       Pretyping.understand sigma env t_hole
-    with 
-    | Loc.Exc_located (loc,Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _)) ->
-        resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole)
+    with
+      | Pretype_errors.PretypeError (_,_,Pretype_errors.UnsolvableImplicit _) as e ->
+          let loc = match Loc.get_loc e with None -> Loc.ghost | Some loc -> loc in
+          resolve_hole (subst_hole_with_term (fst (Loc.unloc loc)) c_raw t_hole)
   in
   let t_constr = resolve_hole (subst_var_with_hole occ id t_raw) in
   let t_constr_type = Retyping.get_type_of env sigma t_constr in
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 8b0820c525..fbe11432ea 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1209,7 +1209,6 @@ let cl_rewrite_clause_tac ?abs strat meta clause gl =
       let res = cl_rewrite_clause_aux ?abs strat (pf_env gl) [] sigma concl is_hyp in
 	treat res
     with
-    | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
     | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
 	Refiner.tclFAIL 0
 	  (str"Unable to satisfy the rewriting constraints."
@@ -1300,7 +1299,6 @@ let cl_rewrite_clause_newtac ?abs strat clause =
 	       cl_rewrite_clause_aux ?abs strat env [] sigma ty is_hyp 
 	     in return (res, is_hyp)
 	   with
-	   | Loc.Exc_located (_, TypeClassError (env, (UnsatisfiableConstraints _ as e)))
 	   | TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
 	     raise (RewriteFailure (str"Unable to satisfy the rewriting constraints."
 			++ fnl () ++ Himsg.explain_typeclass_error env e)))
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 530f15f34a..274a235599 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -73,8 +73,13 @@ let catch_error call_trace tac g =
   let e = Errors.push e in
   let inner_trace,loc,e = match e with
   | LtacLocated (inner_trace,loc,e) -> inner_trace,loc,e
-  | Loc.Exc_located (loc,e) -> [],loc,e
-  | e -> [],Loc.ghost,e in
+  | e ->
+    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
   else
     raise (LtacLocated(inner_trace@call_trace,loc,e))
@@ -1188,15 +1193,16 @@ and eval_with_fail ist is_lazy goal tac =
 	let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in
 	VRTactic (catch_error trace tac { goal with sigma=sigma })
     | a -> a)
-  with
-    | FailError (0,s) | Loc.Exc_located(_, FailError (0,s))
-    | LtacLocated (_,_,FailError (0,s)) ->
+  with e ->
+    (** FIXME: Should we add [Errors.push]? *)
+    match e with
+    | FailError (0,s) | LtacLocated (_,_,FailError (0,s)) ->
 	raise (Eval_fail (Lazy.force s))
-    | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
-    | Loc.Exc_located(s,FailError (lvl,s')) ->
-	raise (Loc.Exc_located(s,FailError (lvl - 1, s')))
+    | FailError (lvl,s) ->
+      raise (Exninfo.copy e (FailError (lvl - 1, s)))
     | LtacLocated (s'',loc,FailError (lvl,s')) ->
 	raise (LtacLocated (s'',loc,FailError (lvl - 1, s')))
+    | _ -> raise e
 
 (* Interprets the clauses of a recursive LetIn *)
 and interp_letrec ist gl llc u =