aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tactics/tacinterp.ml3
1 files changed, 2 insertions, 1 deletions
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)