From 15c8affb8643d1d6985311b3e303fa41f58f7d24 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 7 Nov 2014 18:58:01 +0100
Subject: Print [uconstr]-s in [idtac] messages.

---
 tactics/tacinterp.ml | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 63eb200de8..d34972fb58 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -799,6 +799,12 @@ let rec message_of_value v =
   else if has_type v (topwit wit_constr_context) then
     let c = out_gen (topwit wit_constr_context) v in
     Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) c) end
+  else if has_type v (topwit wit_uconstr) then
+    let c = out_gen (topwit wit_uconstr) v in
+    Ftactic.nf_enter begin fun gl ->
+      Ftactic.return (pr_closed_glob_env (pf_env gl)
+                        (Proofview.Goal.sigma gl) c)
+    end
   else match Value.to_list v with
   | Some l ->
     Ftactic.List.map message_of_value l >>= fun l ->
-- 
cgit v1.2.3