From a20562873304a657cb7d813c75f9bc34c24dbeb6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 5 Apr 2009 21:46:03 +0000
Subject: 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
---
 CHANGES              | 1 +
 tactics/tacinterp.ml | 4 ++--
 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
-- 
cgit v1.2.3