diff options
| author | courtieu | 2012-10-01 16:17:51 +0000 |
|---|---|---|
| committer | courtieu | 2012-10-01 16:17:51 +0000 |
| commit | d3b2c6f8a6864c44236b1f4b2ac89a025f49b7cd (patch) | |
| tree | 94985eacc1c3b416b9707802a4d2d2f8a5e8d5f9 /plugins/syntax/string_syntax.ml | |
| parent | 4a10b5e505df255a7ff8efa68214a14f50c24576 (diff) | |
Added a new tactical infoH tac, that displays the names of hypothesis created by tac, in the 'as' format. Interfaces can use this to insert automatically an 'as' close at the end of the tactic (afterward).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15839 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/syntax/string_syntax.ml')
0 files changed, 0 insertions, 0 deletions