index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
/
refman
Commit message (
Expand
)
Author
Age
*
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 Print Strategy command.
Pierre-Marie Pédrot
2014-03-20
*
refman: document vi2vo
Enrico Tassi
2014-02-26
*
Removing the [Require "file"] syntax.
Pierre-Marie Pédrot
2014-02-02
*
-schedule-vi-checking ported to spawn
Enrico Tassi
2014-01-26
*
Fixing typo in reference manual from previous commit
Hugo Herbelin
2014-01-13
*
Documenting old but useful command "Print Tables".
Hugo Herbelin
2014-01-13
*
refman: fist stab at Asynchronous Proofs
Enrico Tassi
2014-01-05
*
Reference the 'external' tactic.
Guillaume Melquiond
2014-01-01
*
micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...
Frédéric Besson
2013-12-20
*
Documenting the tactic-in-term construction.
Pierre-Marie Pédrot
2013-12-11
*
Missing file in commit 1fb883.
Arnaud Spiwack
2013-12-06
*
Documentation of the Derive plugin.
Arnaud Spiwack
2013-12-04
*
Silence some warning about references in documentation.
Guillaume Melquiond
2013-12-03
*
First stab at documenting Canonical Structures
Enrico Tassi
2013-11-29
*
Fix ltac's progress tactical: requires progress in each goal.
aspiwack
2013-11-04
*
Doc: solve the bad interaction between Declare Implicit Tactic and refine.
aspiwack
2013-11-02
*
Documentation for the backtracking features.
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
*
Updating documentation of the ring/field tactics.
amahboub
2013-08-23
*
Manual fixed w.r.t. STM
gareuselesinge
2013-08-08
*
Documenting the Remove Hints command.
ppedrot
2013-08-01
*
Documenting the previous commit: Existing Instance with priority.
ppedrot
2013-08-01
*
Revising r16550 about providing intro patterns for applying injection:
herbelin
2013-07-09
*
Documenting a potential source of incompleteness in the ring tactic,
amahboub
2013-06-17
*
Fixing #3056
ppedrot
2013-06-06
*
Document changes and add missing documentation for Program options.
msozeau
2013-06-06
*
Start documenting new [rewrite_strat] tactic that applies rewriting
msozeau
2013-06-04
*
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 "appcontext" by default.
ppedrot
2013-05-29
*
Documenting the previous commit.
ppedrot
2013-05-12
*
Fix typo in manual
gareuselesinge
2013-05-06
*
Renaming SearchAbout into Search and Search into SearchHead.
herbelin
2013-04-17
*
Small doc fix : module subtyping cannot force access of opaques
letouzey
2013-04-04
*
Revised infrastructure for lazy loading of opaque proofs
letouzey
2013-04-02
*
Typo in refman (fix #2962)
letouzey
2013-03-25
*
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
*
Allowing (Co)Fixpoint to be defined local and Let-style.
ppedrot
2013-03-11
*
Documentation of the "Local Definition" command.
ppedrot
2013-03-11
*
Added missing documentation of Set Printing Existential Instances.
herbelin
2013-02-21
*
Documenting the 'Printing Transparent/All Dependencies' command.
ppedrot
2012-10-30
*
RefMan-tac: fix a few glitches concerning the documentation of eqn:
letouzey
2012-10-23
[next]