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 /proofs/refiner.mli | |
| 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 'proofs/refiner.mli')
| -rw-r--r-- | proofs/refiner.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/proofs/refiner.mli b/proofs/refiner.mli index 4e30c9c0b..b5fc9ee66 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.mli @@ -136,6 +136,7 @@ val tclDO : int -> tactic -> tactic val tclTIMEOUT : int -> tactic -> tactic val tclWEAK_PROGRESS : tactic -> tactic val tclPROGRESS : tactic -> tactic +val tclSHOWHYPS : tactic -> tactic val tclNOTSAMEGOAL : tactic -> tactic (** [tclIFTHENELSE tac1 tac2 tac3 gls] first applies [tac1] to [gls] then, |