diff options
| author | herbelin | 2009-04-05 21:46:03 +0000 |
|---|---|---|
| committer | herbelin | 2009-04-05 21:46:03 +0000 |
| commit | a20562873304a657cb7d813c75f9bc34c24dbeb6 (patch) | |
| tree | 05c68d7b3f96410a032312efa134956deee19225 /CHANGES | |
| parent | 57cb2e40d0fb6e65a82fd1cda7930b7a6f743c8f (diff) | |
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
Diffstat (limited to 'CHANGES')
| -rw-r--r-- | CHANGES | 1 |
1 files changed, 1 insertions, 0 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 |