Fixing nice printing of error reporting with ml tactics bound to ltac names.

4 files changed, 27 insertions, 19 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index a655bc5266..703c446478 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -192,6 +192,8 @@ Pptactic
 Ppdecl_proof
 Egramml
 Egramcoq
+Tacsubst
+Tacenv
 Himsg
 Cerrors
 Locality
diff --git a/tactics/tacenv.ml b/tactics/tacenv.ml
index 8557ee6a80..3905708172 100644
--- a/tactics/tacenv.ml
+++ b/tactics/tacenv.ml
@@ -75,43 +75,45 @@ open Libnames
 open Libobject
 
 let mactab =
-  Summary.ref (KNmap.empty : glob_tactic_expr KNmap.t)
+  Summary.ref (KNmap.empty : (bool * glob_tactic_expr) KNmap.t)
     ~name:"tactic-definition"
 
-let interp_ltac r = KNmap.find r !mactab
+let interp_ltac r = snd (KNmap.find r !mactab)
+
+let is_ltac_for_ml_tactic r = fst (KNmap.find r !mactab)
 
 (* Declaration of the TAC-DEFINITION object *)
 let add (kn,td) = mactab := KNmap.add kn td !mactab
 let replace (kn,td) = mactab := KNmap.add kn td !mactab
 
-let load_md i ((sp, kn), (local, id ,t)) = match id with
+let load_md i ((sp, kn), (local, id, b, t)) = match id with
 | None ->
   let () = if not local then Nametab.push_tactic (Until i) sp kn in
-  add (kn, t)
-| Some kn -> add (kn, t)
+  add (kn, (b,t))
+| Some kn -> add (kn, (b,t))
 
-let open_md i ((sp, kn), (local, id ,t)) = match id with
+let open_md i ((sp, kn), (local, id, b, t)) = match id with
 | None ->
   let () = if not local then Nametab.push_tactic (Exactly i) sp kn in
-  add (kn, t)
-| Some kn -> add (kn, t)
+  add (kn, (b,t))
+| Some kn -> add (kn, (b,t))
 
-let cache_md ((sp, kn), (local, id ,t)) = match id with
+let cache_md ((sp, kn), (local, id ,b, t)) = match id with
 | None ->
   let () = Nametab.push_tactic (Until 1) sp kn in
-  add (kn, t)
-| Some kn -> add (kn, t)
+  add (kn, (b,t))
+| Some kn -> add (kn, (b,t))
 
 let subst_kind subst id = match id with
 | None -> None
 | Some kn -> Some (Mod_subst.subst_kn subst kn)
 
-let subst_md (subst, (local, id, t)) =
-  (local, subst_kind subst id, Tacsubst.subst_tactic subst t)
+let subst_md (subst, (local, id, b, t)) =
+  (local, subst_kind subst id, b, Tacsubst.subst_tactic subst t)
 
-let classify_md (local, _, _ as o) = Substitute o
+let classify_md (local, _, _, _ as o) = Substitute o
 
-let inMD : bool * Nametab.ltac_constant option * glob_tactic_expr -> obj =
+let inMD : bool * Nametab.ltac_constant option * bool * glob_tactic_expr -> obj =
   declare_object {(default_object "TAC-DEFINITION") with
      cache_function  = cache_md;
      load_function   = load_md;
@@ -119,8 +121,8 @@ let inMD : bool * Nametab.ltac_constant option * glob_tactic_expr -> obj =
      subst_function = subst_md;
      classify_function = classify_md}
 
-let register_ltac local id tac =
-  ignore (Lib.add_leaf id (inMD (local, None, tac)))
+let register_ltac ?(for_ml=false) local id tac =
+  ignore (Lib.add_leaf id (inMD (local, None, for_ml, tac)))
 
 let redefine_ltac local kn tac =
-  Lib.add_anonymous_leaf (inMD (local, Some kn, tac))
+  Lib.add_anonymous_leaf (inMD (local, Some kn, false, tac))
diff --git a/tactics/tacenv.mli b/tactics/tacenv.mli
index 841e1b390f..d65177c5cd 100644
--- a/tactics/tacenv.mli
+++ b/tactics/tacenv.mli
@@ -25,7 +25,7 @@ val interp_alias : alias -> glob_tactic_expr
 
 (** {5 Coq tactic definitions} *)
 
-val register_ltac : bool -> Id.t -> glob_tactic_expr -> unit
+val register_ltac : ?for_ml:bool -> bool -> Id.t -> glob_tactic_expr -> unit
 (** Register a new Ltac with the given name and body. If the boolean flag is set
     to true, then this is a local definition. It also puts the Ltac name in the
     nametab, so that it can be used unqualified. *)
@@ -37,6 +37,8 @@ val redefine_ltac : bool -> KerName.t -> glob_tactic_expr -> unit
 val interp_ltac : KerName.t -> glob_tactic_expr
 (** Find a user-defined tactic by name. Raise [Not_found] if it is absent. *)
 
+val is_ltac_for_ml_tactic : KerName.t -> bool
+
 (** {5 ML tactic extensions} *)
 
 type ml_tactic =
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 7962e52bad..f3768ae922 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1217,6 +1217,8 @@ let explain_ltac_call_trace last trace loc =
 
 let skip_extensions trace =
   let rec aux = function
+  | (_,Proof_type.LtacNameCall f as tac) :: _ 
+      when Tacenv.is_ltac_for_ml_tactic f -> [tac]
   | (_,(Proof_type.LtacNotationCall _ | Proof_type.LtacMLCall _) as tac)
       :: _ -> [tac]
   | t :: tail -> t :: aux tail