From 47bf10e0216f7736ffe7921ce74d620594bcfcba Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 5 Jun 2016 11:18:05 +0200
Subject: About printing of traces of failures while calling ltac code.

An Ltac trace printing mechanism was introduced in 8.4 which was
inadvertedly modified by a series of commits such as 8e10368c3,
91f44f1da7a, ...

It was also sometimes buggy, iirc, when entering ML tactics which
themselves were calling ltac code.

It got really bad in 8.5 as in:

Tactic Notation "f" constr(x) := apply x. Ltac g x := f x.
Goal False.
idtac; f I. (* bad location reporting *)
g I.        (* was referring to tactic name "Top.Top#<>#1" *)

which this commit fixes.

I don't have a clear idea of what would be the best ltac tracing
mechanism, but to avoid it to be broken without being noticed, I
started to add some tests.

Eventually, it might be worth that an Ltac expert brainstrom on it!
---
 printing/pptactic.ml     | 18 ++++++++++++++++++
 printing/pptacticsig.mli |  2 ++
 2 files changed, 20 insertions(+)

(limited to 'printing')

diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 114410fed1..3d1e3e054f 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -366,6 +366,24 @@ module Make
       in
       str "<" ++ name ++ str ">" ++ args
 
+
+  let pr_alias_key key =
+    try
+      let prods = (KNmap.find key !prnotation_tab).pptac_prods in
+      (* First printing strategy: only the head symbol *)
+      match prods with
+      | TacTerm s :: prods -> str s
+      | _ ->
+      (* Second printing strategy; if ever Tactic Notation is eventually *)
+      (* accepting notations not starting with an identifier *)
+      let rec pr = function
+      | [] -> []
+      | TacTerm s :: prods -> s :: pr prods
+      | TacNonTerm (_,_,id) :: prods -> ".." :: pr prods in
+      str (String.concat " " (pr prods))
+    with Not_found ->
+      KerName.print key
+    
   let pr_alias_gen pr_gen lev key l =
     try
       let pp = KNmap.find key !prnotation_tab in
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index 4ef2ea9189..f02785a554 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -45,6 +45,8 @@ module type Pp = sig
   val pr_extend :
     (Val.t -> std_ppcmds) -> int -> ml_tactic_entry -> Val.t list -> std_ppcmds
 
+  val pr_alias_key : Names.KerName.t -> std_ppcmds
+
   val pr_alias : (Val.t -> std_ppcmds) ->
     int -> Names.KerName.t -> Val.t list -> std_ppcmds
 
-- 
cgit v1.2.3