index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
doc
/
refman
/
RefMan-tac.tex
Age
Commit message (
Expand
)
Author
2014-11-16
Enforcing a stronger difference between the two syntaxes "simpl
Hugo Herbelin
2014-11-07
Fixing doc of Functional Induction.
Hugo Herbelin
2014-11-04
Documenting the change of semantics of the replace tactic.
Pierre-Marie Pédrot
2014-10-24
Addressing report #3279 (inconsistency of behavior of the -> and <-
Hugo Herbelin
2014-09-10
Fixing inversion after having fixed intros_replacing
Hugo Herbelin
2014-09-10
Removing "eqn:" for "induction" in reference manual.
Hugo Herbelin
2014-09-08
Doc: [revgoals].
Arnaud Spiwack
2014-09-07
Little fix in documentation of inversion.
Hugo Herbelin
2014-09-03
Cbn in refman
Pierre Boutillier
2014-08-25
"allows to", like "allowing to", is improper
Jason Gross
2014-08-18
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-05
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-07-31
Typos.
Hugo Herbelin
2014-07-25
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-05-31
More on injection over a projectable "existT". - Fixing syntax "injection ......
Hugo Herbelin
2014-04-04
Fix for bug #3107.
Guillaume Melquiond
2014-04-04
fixing Function doc
Julien Forest
2014-04-02
Fix Bug 3131 + Really drop mentions of info in refman.
Pierre Boutillier
2013-12-11
Documenting the tactic-in-term construction.
Pierre-Marie Pédrot
2013-12-03
Silence some warning about references in documentation.
Guillaume Melquiond
2013-11-02
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-08-30
add "Print Ring" and "Print Field" vernacular commands
gareuselesinge
2013-08-08
Manual fixed w.r.t. STM
gareuselesinge
2013-08-01
Documenting the Remove Hints command.
ppedrot
2013-07-09
Revising r16550 about providing intro patterns for applying injection:
herbelin
2013-06-02
Making the behavior of "injection ... as ..." more natural:
herbelin
2013-06-02
Fixing a typo in the documentation of discriminate.
herbelin
2013-05-12
Documenting the previous commit.
ppedrot
2013-05-06
Fix typo in manual
gareuselesinge
2013-03-21
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
2012-10-23
RefMan-tac: fix a few glitches concerning the documentation of eqn:
letouzey
2012-09-16
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-15
Port rewrites of tactic documentation from branch 8.4.
gmelquio
2012-08-11
Improving rendering of ldots in doc (partially done, there are too
herbelin
2012-07-09
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-05
Open Local Scope ---> Local Open Scope, same with Notation and alii
letouzey
[next]
