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
*
Document swap tactic.
Arnaud Spiwack
2014-07-25
*
Document cycle tactic.
Arnaud Spiwack
2014-07-25
*
Update the documentation of Ltac's ";" and ";[…]" to reflect the new multi-...
Arnaud Spiwack
2014-07-25
*
Warns about inconsistency of generated name in evars and goals.
Arnaud Spiwack
2014-07-25
*
More documentation of universes.
Matthieu Sozeau
2014-07-25
*
Start documenting universe polymorphism.
Matthieu Sozeau
2014-07-24
*
Derive plugin: document new syntax.
Arnaud Spiwack
2014-07-23
*
Documenting the changes of Locate semantics.
Pierre-Marie Pédrot
2014-07-21
*
Adding a "time" tactical for benchmarking purposes. In case the tactic
Hugo Herbelin
2014-07-13
*
Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes"
Hugo Herbelin
2014-07-01
*
Fixing grammar in doc of Opaque as proposed by Jason (#3389).
Hugo Herbelin
2014-06-21
*
Deprecate useless option -quality.
Guillaume Melquiond
2014-06-13
*
Remove documentation for the unsupported options -byte and -opt.
Guillaume Melquiond
2014-06-13
*
Deprecate options -dont, -lazy, -force-load-proofs.
Guillaume Melquiond
2014-06-13
*
More on injection over a projectable "existT". - Fixing syntax "injection ......
Hugo Herbelin
2014-05-31
*
Typo reference manual
Hugo Herbelin
2014-05-08
*
Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)
Guillaume Melquiond
2014-04-28
*
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
[next]