aboutsummaryrefslogtreecommitdiffhomepage
path: root/doc
Commit message (Expand)AuthorAge
* Update of Extraction documentationGravatar letouzey2010-06-14
* Extraction Implicit: documentationGravatar letouzey2010-06-14
* Reverted commit 13110 about headers.sty that I wrongly thought was buggy. Sorry.Gravatar herbelin2010-06-11
* Fixed a very old (from V6.3) typo in headers.styGravatar herbelin2010-06-10
* Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".Gravatar herbelin2010-06-08
* Backporting part of r12970 to trunk (deprecation of double induction).Gravatar herbelin2010-06-07
* doc Nstaz updatedGravatar pottier2010-06-04
* A new command Compute foo, shortcut for Eval vm_compute in fooGravatar letouzey2010-06-04
* ajout oublieGravatar pottier2010-06-03
* plugin groebner updated and renamed as nsatz; first version of the doc of nsa...Gravatar pottier2010-06-03
* Minor fix in doc chapter on inference rules (added a missing space).Gravatar herbelin2010-05-28
* Extract Inductive is now possible toward non-inductive types (e.g. nat => int)Gravatar letouzey2010-05-21
* Remove compile-command pragmas for emacsGravatar letouzey2010-05-19
* Some ocamldoc comments + Fixing name of .coqrc.version file in refmanGravatar pboutill2010-05-18
* Update of credits filesGravatar herbelin2010-05-09
* Correction in Function documentationGravatar jforest2010-05-06
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* small detail about Scheme Equality Gravatar vsiles2010-04-27
* Applying François Garillot's patch (#2261 in bug tracker) for extendedGravatar herbelin2010-04-22
* Documenting the use of ##, %%, $$ in coqdoc.Gravatar herbelin2010-04-09
* Applied Cédric Auger's patch to fix use of "#&xxx;" in html printingGravatar herbelin2010-04-09
* Add documentation on the treatment of [if] and [let (x1, ... xn) := ..]Gravatar msozeau2010-03-31
* Update manual on search commandsGravatar puech2010-03-11
* Correction du bug #2214 + maj liens webGravatar notin2010-02-26
* Polishing the setup of CoqIDE Input MethodGravatar vgross2010-02-18
* Documentation of the ! annotation for functor applicationGravatar letouzey2010-02-11
* Fix [Existing Class] impl and add documentation. Fix computation of theGravatar msozeau2010-02-10
* Update CHANGES, add documentation for new commands/tactics and do a bitGravatar msozeau2010-01-30
* New command Declare Reduction <id> := <conv_expr>.Gravatar letouzey2010-01-28
* Document Local Declare ML ModuleGravatar glondu2010-01-14
* Include can accept both Module and Module TypeGravatar letouzey2010-01-07
* Specific syntax for Instances in Module Type: Declare InstanceGravatar letouzey2010-01-04
* Patches and instructions to enable Input Method support in CoqIDE.Gravatar vgross2009-12-21
* Description of the new features of the module system (part two).Gravatar soubiran2009-12-15
* Description of the new features of the module system (first part).Gravatar soubiran2009-12-15
* Document Generalizable Variables, and change syntax to Gravatar msozeau2009-11-15
* 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