Revised the Ltac trace mechanism so that trace breaking due to

interleaving of ltac and ml code is not visible (this particularly
applies to ltac notation ring, which calls ml-level ring_lookup and
Ring again at the ltac level, resulting in non-localisation of "ring"
errors).

Added also missing LtacLocated checks in Class_instance and Proofview.

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

2 files changed, 26 insertions, 20 deletions

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 53a284fa88..c70351caaf 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -196,6 +196,7 @@ 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
 
 let nb_empty_evars s =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f780ca79f5..530f15f34a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -69,19 +69,15 @@ type value =
 let dloc = Loc.ghost
 
 let catch_error call_trace tac g =
-  if List.is_empty call_trace then tac g else try tac g with
-  | LtacLocated _ as e -> let e = Errors.push e in raise e
-  | Loc.Exc_located (_,LtacLocated _) as e ->
-    let e = Errors.push e in raise e
-  | e ->
-    let e = Errors.push e in
-    let (nrep,loc',c),tail = List.sep_last call_trace in
-    let loc,e' = match e with Loc.Exc_located(loc,e) -> loc,e | _ ->dloc,e in
-    if List.is_empty tail then
-      let loc = if Loc.is_ghost loc then loc' else loc in
-      raise (Loc.Exc_located(loc,e'))
-    else
-      raise (Loc.Exc_located(loc',LtacLocated((nrep,c,tail,loc),e')))
+  try tac g with e ->
+  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
+  if List.is_empty call_trace & List.is_empty inner_trace then raise e
+  else
+    raise (LtacLocated(inner_trace@call_trace,loc,e))
 
 (* Signature for interpretation: val_interp and interpretation functions *)
 type interp_sign =
@@ -161,6 +157,10 @@ let propagate_trace ist loc id = function
       VFun (push_trace(loc,LtacVarCall (id,t)) ist.trace,lfun,it,b)
   | x -> x
 
+let append_trace trace = function
+  | VFun (trace',lfun,it,b) -> VFun (trace'@trace,lfun,it,b)
+  | x -> x
+
 (* Dynamically check that an argument is a tactic *)
 let coerce_to_tactic loc id = function
   | VFun _ | VRTactic _ as a -> a
@@ -469,7 +469,8 @@ let interp_gen kind ist allow_patvar expand_evar fail_evar use_classes env sigma
       let ltacdata = (List.map fst ltacvars,unbndltacvars) in
       intern_gen kind ~allow_patvar ~ltacvars:ltacdata sigma env c
   in
-  let trace = push_trace (dloc,LtacConstrInterp (c,vars)) ist.trace in
+  let trace =
+    push_trace (loc_of_glob_constr c,LtacConstrInterp (c,vars)) ist.trace in
   let evdc =
     catch_error trace 
       (understand_ltac ~resolve_classes:use_classes expand_evar sigma env vars kind) c 
@@ -1139,14 +1140,18 @@ and interp_app loc ist gl fv largs =
          (TacFun _|TacLetIn _|TacMatchGoal _|TacMatch _| TacArg _ as body))) ->
 	let (newlfun,lvar,lval)=head_with_value (var,largs) in
 	if List.is_empty lvar then
+          (* Check evaluation and report problems with current trace *)
 	  let (sigma,v) =
 	    try
-	      catch_error trace
-		(val_interp {ist with lfun=newlfun@olfun; trace=trace} gl) body
+              catch_error trace
+		(val_interp {ist with lfun=newlfun@olfun; trace=[]} gl) body
 	    with e ->
               let e = Errors.push e in
               debugging_exception_step ist false e (fun () -> str "evaluation");
 	      raise e in
+          (* No errors happened, we propagate the trace *)
+          let v = append_trace trace v in
+
 	  let gl = { gl with sigma=sigma } in
           debugging_step ist
 	    (fun () ->
@@ -1163,7 +1168,7 @@ and tactic_of_value ist vle g =
   match vle with
   | VRTactic res -> res
   | VFun (trace,lfun,[],t) ->
-      let tac = eval_tactic {ist with lfun=lfun; trace=trace} t in
+      let tac = eval_tactic {ist with lfun=lfun; trace=[]} t in
       catch_error trace tac g
   | (VFun _|VRec _) -> error "A fully applied tactic is expected."
   | VConstr _ -> errorlabstrm "" (str"Value is a term. Expected a tactic.")
@@ -1185,13 +1190,13 @@ and eval_with_fail ist is_lazy goal tac =
     | a -> a)
   with
     | FailError (0,s) | Loc.Exc_located(_, FailError (0,s))
-    | Loc.Exc_located(_,LtacLocated (_,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')))
-    | Loc.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) ->
-	raise (Loc.Exc_located(s,LtacLocated (s'',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 =