Display the content of the list instead of "<list>" when an idtac

argument is a variable bound to a list (see S. Lescuyer's message on
coq-club, Apr 5, 2009).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12050 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 3 insertions, 2 deletions

diff --git a/CHANGES b/CHANGES
index 5ac505f0e2..d83ce42af4 100644
--- a/CHANGES
+++ b/CHANGES
@@ -14,6 +14,7 @@ Tactics
   "destruct" (rare source of incompatibility).
 - Tactic "quote" now supports quotation of arbitrary terms (not just the
   goal).
+- Tactic "idtac" now displays its list arguments.
 
 Vernacular commands
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 29b71fad43..6fe7b9288a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1625,13 +1625,13 @@ let inj_may_eval = function
   | ConstrContext (id,c) -> ConstrContext (id,inj_open c)
   | ConstrTypeOf c -> ConstrTypeOf (inj_open c)
 
-let message_of_value = function
+let rec message_of_value = function
   | VVoid -> str "()"
   | VInteger n -> int n
   | VIntroPattern ipat -> pr_intro_pattern (dloc,ipat)
   | VConstr_context c | VConstr c -> pr_constr c
   | VRec _ | VRTactic _ | VFun _ -> str "<tactic>"
-  | VList _ -> str "<list>"
+  | VList l -> prlist_with_sep spc message_of_value l
 
 let rec interp_message_token ist = function
   | MsgString s -> str s