aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Prevent coq_tex from generating curly quotes. (Partial fix for bug #2964)Gravatar Guillaume Melquiond2014-04-28
* Completing text of the question on conservativity of CIC over CC (bug #2697).Gravatar Hugo Herbelin2014-04-05
* Fix for bug #3107.Gravatar Guillaume Melquiond2014-04-04
* fixing Function docGravatar Julien Forest2014-04-04
* Fix Bug 3131 + Really drop mentions of info in refman.Gravatar Pierre Boutillier2014-04-02
* Documenting the Print Strategy command.Gravatar Pierre-Marie Pédrot2014-03-20
* refman: document vi2voGravatar Enrico Tassi2014-02-26
* fixup complement FinGravatar Pierre Boutillier2014-02-24
* Removing the [Require "file"] syntax.Gravatar Pierre-Marie Pédrot2014-02-02
* -schedule-vi-checking ported to spawnGravatar Enrico Tassi2014-01-26
* Fixing typo in reference manual from previous commitGravatar Hugo Herbelin2014-01-13
* Documenting old but useful command "Print Tables".Gravatar Hugo Herbelin2014-01-13
* refman: fist stab at Asynchronous ProofsGravatar Enrico Tassi2014-01-05
* Reference the 'external' tactic.Gravatar Guillaume Melquiond2014-01-01
* micromega: removal of spurious Export; addition of Lia.v encapsulating lia an...Gravatar Frédéric Besson2013-12-20
* Documenting the tactic-in-term construction.Gravatar Pierre-Marie Pédrot2013-12-11
* Missing file in commit 1fb883.Gravatar Arnaud Spiwack2013-12-06
* Documentation of the Derive plugin.Gravatar Arnaud Spiwack2013-12-04
* Silence some warning about references in documentation.Gravatar Guillaume Melquiond2013-12-03
* First stab at documenting Canonical StructuresGravatar Enrico Tassi2013-11-29
* Fix ltac's progress tactical: requires progress in each goal.Gravatar aspiwack2013-11-04
* Doc: solve the bad interaction between Declare Implicit Tactic and refine.Gravatar aspiwack2013-11-02
* Documentation for the backtracking features.Gravatar aspiwack2013-11-02
* Adds a tactic give_up.Gravatar aspiwack2013-11-02
* A tactic shelve_unifiable.Gravatar aspiwack2013-11-02
* Adds a shelve tactic.Gravatar aspiwack2013-11-02
* Document "all:" and "Set Default Goal Selector".Gravatar aspiwack2013-11-02
* add "Print Ring" and "Print Field" vernacular commandsGravatar gareuselesinge2013-08-30
* Updating documentation of the ring/field tactics.Gravatar amahboub2013-08-23
* Manual fixed w.r.t. STMGravatar gareuselesinge2013-08-08
* Documenting the Remove Hints command.Gravatar ppedrot2013-08-01
* Documenting the previous commit: Existing Instance with priority.Gravatar ppedrot2013-08-01
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
* Documenting a potential source of incompleteness in the ring tactic,Gravatar amahboub2013-06-17
* Fixing #3056Gravatar ppedrot2013-06-06
* Document changes and add missing documentation for Program options.Gravatar msozeau2013-06-06
* Start documenting new [rewrite_strat] tactic that applies rewritingGravatar msozeau2013-06-04
* A constructive proof of Fan theorem where paths are represented by predicates.Gravatar herbelin2013-06-02
* Making the behavior of "injection ... as ..." more natural:Gravatar herbelin2013-06-02
* Fixing a typo in the documentation of discriminate.Gravatar herbelin2013-06-02
* Documenting the "appcontext" by default.Gravatar ppedrot2013-05-29
* Documenting the previous commit.Gravatar ppedrot2013-05-12
* Fix typo in manualGravatar gareuselesinge2013-05-06
* Renaming SearchAbout into Search and Search into SearchHead.Gravatar herbelin2013-04-17
* Small doc fix : module subtyping cannot force access of opaquesGravatar letouzey2013-04-04
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* Typo in refman (fix #2962)Gravatar letouzey2013-03-25
* Using hnf instead of "intro H" for forcing reduction to a product.Gravatar herbelin2013-03-21
* Fixing an old pecularity of "red": head betaiota redexes are nowGravatar herbelin2013-03-21
* Allowing (Co)Fixpoint to be defined local and Let-style.Gravatar ppedrot2013-03-11