index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
Commit message (
Expand
)
Author
Age
*
Added a (constructive) proof of Weak Konig's lemma for decidable trees.
Hugo Herbelin
2014-07-15
*
Adding a "time" tactical for benchmarking purposes. In case the tactic
Hugo Herbelin
2014-07-13
*
Arith: full integration of the "Numbers" modular framework
Pierre Letouzey
2014-07-09
*
Continuing ff9f94634 on making code and doc agree on "Set Equality Schemes"
Hugo Herbelin
2014-07-01
*
Avoid scanning .coq-native directories when building the library index.
Guillaume Melquiond
2014-06-26
*
Fix documentation.
Guillaume Melquiond
2014-06-26
*
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
*
- Fix index-list to show computational relations for rewriting files.
Matthieu Sozeau
2014-05-06
*
Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)
Guillaume Melquiond
2014-04-28
*
Completing text of the question on conservativity of CIC over CC (bug #2697).
Hugo Herbelin
2014-04-05
*
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
*
fixup complement Fin
Pierre Boutillier
2014-02-24
*
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
[next]