Fixing localisation of tactic errors (my mistake in himsg.ml essentially).

4 files changed, 13 insertions, 4 deletions

diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 76459a59a..2f0b0e608 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -45,6 +45,7 @@ type rule = prim_rule
 (** Ltac traces *)
 
 type ltac_call_kind =
+  | LtacMLCall of glob_tactic_expr
   | LtacNotationCall of KerName.t
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index bbb2c8e09..5fcdddeac 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -68,6 +68,7 @@ type tactic = goal sigma -> goal list sigma
 (** TODO: Move those definitions somewhere sensible *)
 
 type ltac_call_kind =
+  | LtacMLCall of glob_tactic_expr
   | LtacNotationCall of KerName.t
   | LtacNameCall of ltac_constant
   | LtacAtomCall of glob_atomic_tactic_expr
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3fcf38117..c1df201a3 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1216,6 +1216,8 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       Ftactic.run tac (fun v -> tactic_of_value ist v)
 
   | TacML (loc,opn,l) when List.for_all global_genarg l ->
+      let trace = push_trace (loc,LtacMLCall tac) ist in
+      let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
       (* spiwack: a special case for tactics (from TACTIC EXTEND) when
          every argument can be interpreted without a
          [Proofview.Goal.nf_enter]. *)
@@ -1227,8 +1229,10 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       let goal = sig_it Goal.V82.dummy_goal in
       (* /dummy values *)
       let args = List.map (fun a -> snd(interp_genarg ist env sigma concl goal a)) l in
-      tac args ist
+      catch_error_tac trace (tac args ist)
   | TacML (loc,opn,l) ->
+      let trace = push_trace (loc,LtacMLCall tac) ist in
+      let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
       Proofview.Goal.nf_enter begin fun gl ->
         let env = Proofview.Goal.env gl in
         let goal_sigma = Proofview.Goal.sigma gl in
@@ -1240,7 +1244,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
             (fun a sigma -> interp_genarg ist env sigma concl goal a) l goal_sigma
         in
         Proofview.V82.tclEVARS sigma <*>
-        tac args ist
+        catch_error_tac trace (tac args ist)
       end
 
 and force_vrec ist v : typed_generic_argument Ftactic.t =
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 11abe0950..e7be7b479 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1188,6 +1188,8 @@ let explain_ltac_call_trace last trace loc =
   let pr_call ck = match ck with
   | Proof_type.LtacNotationCall kn -> quote (KerName.print kn)
   | Proof_type.LtacNameCall cst -> quote (Pptactic.pr_ltac_constant cst)
+  | Proof_type.LtacMLCall t ->
+      quote (Pptactic.pr_glob_tactic (Global.env()) t)
   | Proof_type.LtacVarCall (id,t) ->
       quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
         Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
@@ -1215,9 +1217,10 @@ let explain_ltac_call_trace last trace loc =
            pr_enum pr_call calls ++ strbrk kind_of_last_call)
 
 let skip_extensions trace =
-  (** FIXME: handle TacAlias & TacML *)
   let rec aux = function
-  | _ :: tail -> aux tail
+  | (_,(Proof_type.LtacNotationCall _ | Proof_type.LtacMLCall _) as tac)
+      :: _ -> [tac]
+  | t :: tail -> t :: aux tail
   | [] -> [] in
   List.rev (aux (List.rev trace))