From a14a74be3fbe621095aa95a58b4ec8e4bf0b591a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 9 Sep 2014 18:55:02 +0200
Subject: Displaying genarg tag in idtac.

---
 tactics/tacinterp.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 85d0ac4cd7..3fcf38117b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -748,7 +748,8 @@ let rec message_of_value v =
     Ftactic.List.map message_of_value l >>= fun l ->
     Ftactic.return (prlist_with_sep spc (fun x -> x) l)
   | None ->
-    Ftactic.return (str "<abstr>") (** TODO *)
+    let tag = pr_argument_type (genarg_tag v) in
+    Ftactic.return (str "<" ++ tag ++ str ">") (** TODO *)
 
 let interp_message_token ist = function
   | MsgString s -> Ftactic.return (str s)
-- 
cgit v1.2.3