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

4 files changed, 44 insertions, 13 deletions

diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 3739b0e4da..790520e97d 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -117,11 +117,15 @@ let rec process_vernac_interp_error = function
            if Int.equal i 0 then str "." else str " (level " ++ int i ++ str").")
   | AlreadyDeclared msg ->
       wrap_vernac_error (msg ++ str ".")
-  | Proof_type.LtacLocated (_,(Refiner.FailError (i,s) as exc)) when not (is_mt s) ->
+  | Proof_type.LtacLocated (_,_,(Refiner.FailError (i,s) as exc)) when not (is_mt s) ->
+      (* Ltac error is intended, trace is irrelevant *)
       process_vernac_interp_error exc
-  | Proof_type.LtacLocated (s,exc) ->
-      EvaluatedError (hov 0 (Himsg.explain_ltac_call_trace s ++ fnl()),
-        Some (process_vernac_interp_error exc))
+  | Proof_type.LtacLocated (s,loc,exc) ->
+      (match
+          Himsg.extract_ltac_trace s loc (process_vernac_interp_error exc)
+       with
+       | None,loc,e -> Loc.Exc_located (loc,e)
+       | Some msg, loc, e -> Loc.Exc_located (loc,EvaluatedError (msg,Some e)))
   | Loc.Exc_located (loc,exc) ->
       Loc.Exc_located (loc,process_vernac_interp_error exc)
   | exc ->
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 8e6ff1eb76..93c3a3b1ad 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -795,7 +795,7 @@ let explain_refiner_error = function
 
 (* Inductive errors *)
 
-let error_non_strictly_positive env c v  =
+let error_non_strictly_positive env c v =
   let pc = pr_lconstr_env env c in
   let pv = pr_lconstr_env env v in
   str "Non strictly positive occurrence of " ++ pv ++ str " in" ++
@@ -994,6 +994,14 @@ let explain_reduction_tactic_error = function
       spc () ++ str "is not well typed." ++ fnl () ++
       explain_type_error env' Evd.empty e
 
+let is_defined_ltac trace =
+  let rec aux = function
+  | (_,_,Proof_type.LtacNameCall _) :: tail -> true
+  | (_,_,Proof_type.LtacAtomCall _) :: tail -> false
+  | _ :: tail -> aux tail
+  | [] -> false in
+  aux (List.rev trace)
+
 let explain_ltac_call_trace (nrep,last,trace,loc) =
   let calls =
     (nrep,last) :: List.rev (List.map(fun(n,_,ck)->(n,ck))trace)
@@ -1031,3 +1039,23 @@ let explain_ltac_call_trace (nrep,last,trace,loc) =
            pr_enum pr_call calls ++ strbrk kind_of_last_call)
   else
     mt ()
+
+let extract_ltac_trace trace eloc e =
+  let (nrep,loc,c),tail = List.sep_last trace in
+  if is_defined_ltac trace then
+    (* We entered a user-defined tactic,
+       we display the trace with location of the call *)
+    let msg = hov 0 (explain_ltac_call_trace (nrep,c,tail,eloc) ++ fnl()) in
+    Some msg, loc, e
+  else
+    (* We entered a primitive tactic, we don't display trace but
+       report on the finest location *)
+    let best_loc =
+      if not (Loc.is_ghost eloc) then eloc else
+        (* trace is with innermost call coming first *)
+        let rec aux = function
+        | (_,loc,_)::tail when not (Loc.is_ghost loc) -> loc
+        | _::tail -> aux tail
+        | [] -> Loc.ghost in
+        aux trace in
+    None, best_loc, e
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 028c33bd28..bd7fb8973e 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -37,9 +37,8 @@ val explain_pattern_matching_error :
 val explain_reduction_tactic_error :
   Tacred.reduction_tactic_error -> std_ppcmds
 
-val explain_ltac_call_trace :
-  int * Proof_type.ltac_call_kind * Proof_type.ltac_trace * Loc.t ->
-  std_ppcmds
+val extract_ltac_trace :
+  Proof_type.ltac_trace -> Loc.t -> exn -> std_ppcmds option * Loc.t * exn
 
 val explain_module_error : Modops.module_typing_error -> std_ppcmds
 
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 6ec01f5474..7211417a68 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -822,11 +822,11 @@ and solve_obligation_by_tac prg obls i tac =
 	with e ->
           let e = Errors.push e in
           match e with
-          | Loc.Exc_located(_, Proof_type.LtacLocated (_, Refiner.FailError (_, s)))
-          | Loc.Exc_located(_, Refiner.FailError (_, s))
-          | Refiner.FailError (_, s) ->
-              user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
-          | e when is_anomaly e -> raise e
+	  | Proof_type.LtacLocated (_, _, Refiner.FailError (_, s))
+	  | Loc.Exc_located(_, Refiner.FailError (_, s))
+	  | Refiner.FailError (_, s) ->
+	      user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
+	  | e when Errors.is_anomaly e -> raise e
           | e -> false
 
 and solve_prg_obligations prg ?oblset tac =