aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Added support for multiple where-clauses in Inductive and co (see wish #2163).Gravatar herbelin2009-11-11
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.Gravatar gmelquio2009-11-04
* Removed 'Toplevel' language from extraction documentation, since it is not cu...Gravatar gmelquio2009-11-04
* Report de la révision #12208 de la v8.2 (correction du bug #2126)Gravatar notin2009-11-03
* Correction du bug #2175Gravatar notin2009-11-02
* Fixed some typos in the reference manual.Gravatar gmelquio2009-10-29
* Typo in the refmanGravatar puech2009-10-28
* Documentation of the Local and Global modifiers.Gravatar herbelin2009-10-27
* Fix Setoid documentation.Gravatar msozeau2009-10-26
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* Fixing XML doc (COQ_XML not working as an environment variable).Gravatar herbelin2009-10-24
* Repaired bug #2165 (buggy coq example in Tactic Examples doc chapter)Gravatar herbelin2009-10-20
* typo in doc of Extraction BlacklistGravatar letouzey2009-10-15
* Typos.Gravatar gmelquio2009-10-13
* Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'Gravatar letouzey2009-10-08
* Fix the stdlib doc compilation + switch all .v file to utf8Gravatar letouzey2009-09-28
* Micromega doc : psatz Z -> psatz Z 2Gravatar fbesson2009-09-24
* Ltac doc: only variables are accepted as message_tokenGravatar glondu2009-09-23
* Remove useless MonoList.vGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Clarify documentation of ltac repeatGravatar glondu2009-09-17
* - Inductive types in the "using" option of auto/eauto/firstorder areGravatar herbelin2009-09-13
* Add doc of [Context] vernacular.Gravatar msozeau2009-09-11
* Removed Gappa from the external provers supported by the dp plugin. Tactic ga...Gravatar gmelquio2009-09-11
* Added syntax "exists bindings, ..., bindings" for iterated "exists".Gravatar herbelin2009-09-10
* Update coqdoc documentation, CHANGES and add a fix for the proofbox (patchGravatar msozeau2009-09-08
* Fix minor spelling errorGravatar glondu2009-08-29
* git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0...Gravatar fbesson2009-08-25
* Improved parameterization of Coq:Gravatar herbelin2009-08-02
* Add doc for [Print Opaque Dependencies] and a better explanation for theGravatar msozeau2009-06-26
* Report de la révision #12200 (bug #2125)Gravatar notin2009-06-22
* Applying Ian Lynagh's documentation fixes patch (see bug #2112)Gravatar herbelin2009-06-06
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* Backporting 12112 from v8.2 branch to trunk (fixing documentation bugsGravatar herbelin2009-04-28
* Document new quote constructionGravatar glondu2009-03-30
* Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...Gravatar letouzey2009-03-20
* RefMan: a label defined twiceGravatar letouzey2009-03-14
* Coqdep: remove references to obsolete .zi and Require Implementation stuffGravatar letouzey2009-03-14
* doc et CHANGES pour la commande TimeoutGravatar barras2009-03-04
* maj de la faq: correction de l'exemple field qui compilait plus en 8.2, corre...Gravatar jnarboux2009-02-17
* Modification du style du manuel de référenceGravatar notin2009-02-11
* Solves some warning and hides some not-bad ones in doc. It remains aGravatar herbelin2009-01-29
* - Fixed various Overfull in documentation.Gravatar herbelin2009-01-27
* Fixes in the documentation of [dependent induction] and test-suiteGravatar msozeau2009-01-22
* Fixed bug 2030 (bad syntax for "test" in doc compilation) [see 11824Gravatar herbelin2009-01-21
* Added some missing statements for proof folding and correctedGravatar vgross2009-01-20
* Added proof folding into CoqIde. See RefMan for using it.Gravatar vgross2009-01-20