diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 4 |
2 files changed, 3 insertions, 2 deletions
@@ -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 |