diff options
| author |  courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-01 16:17:51 +0000 |
|---|---|---|
| committer | courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-10-01 16:17:51 +0000 |
| commit | d3b2c6f8a6864c44236b1f4b2ac89a025f49b7cd (patch) | |
| tree | 94985eacc1c3b416b9707802a4d2d2f8a5e8d5f9 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_ltac.ml4 | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index 51839ee88..bc2803ae5 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -61,6 +61,7 @@ GEXTEND Gram | IDENT "timeout"; n = int_or_var; ta = tactic_expr -> TacTimeout (n,ta) | IDENT "repeat"; ta = tactic_expr -> TacRepeat ta | IDENT "progress"; ta = tactic_expr -> TacProgress ta + | IDENT "infoH"; ta = tactic_expr -> TacShowHyps ta (*To do: put Abstract in Refiner*) | IDENT "abstract"; tc = NEXT -> TacAbstract (tc,None) | IDENT "abstract"; tc = NEXT; "using"; s = ident -> |