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

14 files changed, 92 insertions, 41 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2f88c79a75..267e9d5bf2 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -42,7 +42,7 @@ open Pretype_errors
 
 let rec catchable_exception = function
   | Loc.Exc_located(_,e) -> catchable_exception e
-  | LtacLocated(_,e) -> catchable_exception e
+  | LtacLocated(_,_,e) -> catchable_exception e
   | Errors.UserError _ | TypeError _ | PretypeError (_,_,TypingError _)
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _ | PretypeError (_,_,VarNotFound _)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index eadf870fb4..af50059b8d 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -57,5 +57,5 @@ type ltac_call_kind =
 
 type ltac_trace = (int * Loc.t * ltac_call_kind) list
 
-exception LtacLocated of (int * ltac_call_kind * ltac_trace * Loc.t) * exn
+exception LtacLocated of ltac_trace * Loc.t * exn
 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 37d5c4544c..7ff1afc224 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -82,4 +82,4 @@ type ltac_call_kind =
 
 type ltac_trace = (int * Loc.t * ltac_call_kind) list
 
-exception LtacLocated of (int * ltac_call_kind * ltac_trace * Loc.t) * exn
+exception LtacLocated of ltac_trace * Loc.t * exn
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 96af73b711..19f289316f 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,10 +1,10 @@
 Goal
 Evar_refiner
 Monads
+Proof_type
 Proofview
 Proof
 Proof_global
-Proof_type
 Redexpr
 Logic
 Refiner
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index bcd51fe2b1..c18c48744e 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -335,6 +335,7 @@ let tclEXTEND tacs1 rtac tacs2 env =
 open Pretype_errors
 let rec catchable_exception = function
   | Loc.Exc_located(_,e) -> catchable_exception e
+  | Proof_type.LtacLocated(_,_,e) -> catchable_exception e
   | Errors.UserError _
   | Type_errors.TypeError _ | PretypeError (_,_,TypingError _)
   | Indrec.RecursionSchemeError _
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index c83d5ca7af..332f255b25 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -217,14 +217,13 @@ let catch_failerror e =
   if catchable_exception e then check_for_interrupt ()
   else match e with
   | FailError (0,_) | Loc.Exc_located(_, FailError (0,_))
-  | Loc.Exc_located(_, LtacLocated (_,FailError (0,_)))  ->
+  | LtacLocated (_,_,FailError (0,_))  ->
       check_for_interrupt ()
   | 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')))
   | e -> raise e
 
 (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
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 =
diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out
index f61b7ecf30..839611b65b 100644
--- a/test-suite/output/Errors.out
+++ b/test-suite/output/Errors.out
@@ -1,2 +1,7 @@
 The command has indeed failed with message:
 => Error: The field t is missing in Top.M.
+The command has indeed failed with message:
+=> Error: Unable to unify "nat" with "True".
+The command has indeed failed with message:
+=> In nested Ltac calls to "f" and "apply x", last call failed.
+   Error: Unable to unify "nat" with "True".
diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v
index 75763f3b47..352c87385f 100644
--- a/test-suite/output/Errors.v
+++ b/test-suite/output/Errors.v
@@ -7,3 +7,12 @@ Parameter t:Type.
 End S.
 Module M : S.
 Fail End M.
+
+(* A simple check of how Ltac trace are used or not *)
+(* Unfortunately, cannot test error location... *)
+
+Ltac f x := apply x.
+Goal True.
+Fail simpl; apply 0.
+Fail simpl; f 0.
+Abort.
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 =