index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
/
refman
/
RefMan-tac.tex
Commit message (
Expand
)
Author
Age
*
refman: avoid label names with whitespace (unsupported in html)
Pierre Letouzey
2014-12-09
*
Enforcing a stronger difference between the two syntaxes "simpl
Hugo Herbelin
2014-11-16
*
Fixing doc of Functional Induction.
Hugo Herbelin
2014-11-07
*
Documenting the change of semantics of the replace tactic.
Pierre-Marie Pédrot
2014-11-04
*
Addressing report #3279 (inconsistency of behavior of the -> and <-
Hugo Herbelin
2014-10-24
*
Fixing inversion after having fixed intros_replacing
Hugo Herbelin
2014-09-10
*
Removing "eqn:" for "induction" in reference manual.
Hugo Herbelin
2014-09-10
*
Doc: [revgoals].
Arnaud Spiwack
2014-09-08
*
Little fix in documentation of inversion.
Hugo Herbelin
2014-09-07
*
Cbn in refman
Pierre Boutillier
2014-09-03
*
"allows to", like "allowing to", is improper
Jason Gross
2014-08-25
*
Adding a new intro-pattern for "apply in" on the fly. Using syntax
Hugo Herbelin
2014-08-18
*
Slight simplification of naming of tactics in equality.ml (hopefully).
Hugo Herbelin
2014-08-18
*
Experimentally adding an option for automatically erasing an
Hugo Herbelin
2014-08-05
*
Adding a syntax "enough" for the variant of "assert" with the order of
Hugo Herbelin
2014-08-05
*
Typos.
Hugo Herbelin
2014-07-31
*
Document swap tactic.
Arnaud Spiwack
2014-07-25
*
Document cycle tactic.
Arnaud Spiwack
2014-07-25
*
Warns about inconsistency of generated name in evars and goals.
Arnaud Spiwack
2014-07-25
*
More on injection over a projectable "existT". - Fixing syntax "injection ......
Hugo Herbelin
2014-05-31
*
Fix for bug #3107.
Guillaume Melquiond
2014-04-04
*
fixing Function doc
Julien Forest
2014-04-04
*
Fix Bug 3131 + Really drop mentions of info in refman.
Pierre Boutillier
2014-04-02
*
Documenting the tactic-in-term construction.
Pierre-Marie Pédrot
2013-12-11
*
Silence some warning about references in documentation.
Guillaume Melquiond
2013-12-03
*
Doc: solve the bad interaction between Declare Implicit Tactic and refine.
aspiwack
2013-11-02
*
Adds a tactic give_up.
aspiwack
2013-11-02
*
A tactic shelve_unifiable.
aspiwack
2013-11-02
*
Adds a shelve tactic.
aspiwack
2013-11-02
*
Document "all:" and "Set Default Goal Selector".
aspiwack
2013-11-02
*
add "Print Ring" and "Print Field" vernacular commands
gareuselesinge
2013-08-30
*
Manual fixed w.r.t. STM
gareuselesinge
2013-08-08
*
Documenting the Remove Hints command.
ppedrot
2013-08-01
*
Revising r16550 about providing intro patterns for applying injection:
herbelin
2013-07-09
*
Making the behavior of "injection ... as ..." more natural:
herbelin
2013-06-02
*
Fixing a typo in the documentation of discriminate.
herbelin
2013-06-02
*
Documenting the previous commit.
ppedrot
2013-05-12
*
Fix typo in manual
gareuselesinge
2013-05-06
*
Using hnf instead of "intro H" for forcing reduction to a product.
herbelin
2013-03-21
*
Fixing an old pecularity of "red": head betaiota redexes are now
herbelin
2013-03-21
*
RefMan-tac: fix a few glitches concerning the documentation of eqn:
letouzey
2012-10-23
*
Move reflexivity, symmetry, and transitivity, next to f_equal, in the documen...
gmelquio
2012-09-16
*
Some more fixes to tactic documentation.
gmelquio
2012-09-16
*
Beautify tactic documentation a bit more.
gmelquio
2012-09-16
*
Remove superfluous spaces and commas in tactic documentation.
gmelquio
2012-09-16
*
Fix index generation for the pdf document.
gmelquio
2012-09-16
*
Port rewrites of tactic documentation from branch 8.4.
gmelquio
2012-09-15
*
Improving rendering of ldots in doc (partially done, there are too
herbelin
2012-08-11
*
The tactic remember now accepts a final eqn:H option (grant wish #2489)
letouzey
2012-07-09
*
induction/destruct : nicer syntax for generating equations (solves #2741)
letouzey
2012-07-09
[next]