coq - The formal proof system

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