| Commit message (Expand) | Author | Age |
* | Remove the svn-specific $Id$ annotations | letouzey | 2010-04-29 |
* | small detail about Scheme Equality | vsiles | 2010-04-27 |
* | Applying François Garillot's patch (#2261 in bug tracker) for extended | herbelin | 2010-04-22 |
* | Documenting the use of ##, %%, $$ in coqdoc. | herbelin | 2010-04-09 |
* | Applied Cédric Auger's patch to fix use of "#&xxx;" in html printing | herbelin | 2010-04-09 |
* | Add documentation on the treatment of [if] and [let (x1, ... xn) := ..] | msozeau | 2010-03-31 |
* | Update manual on search commands | puech | 2010-03-11 |
* | Correction du bug #2214 + maj liens web | notin | 2010-02-26 |
* | Polishing the setup of CoqIDE Input Method | vgross | 2010-02-18 |
* | Documentation of the ! annotation for functor application | letouzey | 2010-02-11 |
* | Fix [Existing Class] impl and add documentation. Fix computation of the | msozeau | 2010-02-10 |
* | Update CHANGES, add documentation for new commands/tactics and do a bit | msozeau | 2010-01-30 |
* | New command Declare Reduction <id> := <conv_expr>. | letouzey | 2010-01-28 |
* | Document Local Declare ML Module | glondu | 2010-01-14 |
* | Include can accept both Module and Module Type | letouzey | 2010-01-07 |
* | Specific syntax for Instances in Module Type: Declare Instance | letouzey | 2010-01-04 |
* | Patches and instructions to enable Input Method support in CoqIDE. | vgross | 2009-12-21 |
* | Description of the new features of the module system (part two). | soubiran | 2009-12-15 |
* | Description of the new features of the module system (first part). | soubiran | 2009-12-15 |
* | Document Generalizable Variables, and change syntax to | msozeau | 2009-11-15 |
* | Added support for multiple where-clauses in Inductive and co (see wish #2163). | herbelin | 2009-11-11 |
* | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin | 2009-11-08 |
* | Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names. | gmelquio | 2009-11-04 |
* | Removed 'Toplevel' language from extraction documentation, since it is not cu... | gmelquio | 2009-11-04 |
* | Report de la révision #12208 de la v8.2 (correction du bug #2126) | notin | 2009-11-03 |
* | Correction du bug #2175 | notin | 2009-11-02 |
* | Fixed some typos in the reference manual. | gmelquio | 2009-10-29 |
* | Typo in the refman | puech | 2009-10-28 |
* | Documentation of the Local and Global modifiers. | herbelin | 2009-10-27 |
* | Fix Setoid documentation. | msozeau | 2009-10-26 |
* | New cleaning phase of the Local/Global option management | herbelin | 2009-10-26 |
* | Improved the treatment of Local/Global options (noneffective Local on | herbelin | 2009-10-25 |
* | Fixing XML doc (COQ_XML not working as an environment variable). | herbelin | 2009-10-24 |
* | Repaired bug #2165 (buggy coq example in Tactic Examples doc chapter) | herbelin | 2009-10-20 |
* | typo in doc of Extraction Blacklist | letouzey | 2009-10-15 |
* | Typos. | gmelquio | 2009-10-13 |
* | Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False' | letouzey | 2009-10-08 |
* | Fix the stdlib doc compilation + switch all .v file to utf8 | letouzey | 2009-09-28 |
* | Micromega doc : psatz Z -> psatz Z 2 | fbesson | 2009-09-24 |
* | Ltac doc: only variables are accepted as message_token | glondu | 2009-09-23 |
* | Remove useless MonoList.v | glondu | 2009-09-17 |
* | Delete trailing whitespaces in all *.{v,ml*} files | glondu | 2009-09-17 |
* | Clarify documentation of ltac repeat | glondu | 2009-09-17 |
* | - Inductive types in the "using" option of auto/eauto/firstorder are | herbelin | 2009-09-13 |
* | Add doc of [Context] vernacular. | msozeau | 2009-09-11 |
* | Removed Gappa from the external provers supported by the dp plugin. Tactic ga... | gmelquio | 2009-09-11 |
* | Added syntax "exists bindings, ..., bindings" for iterated "exists". | herbelin | 2009-09-10 |
* | Update coqdoc documentation, CHANGES and add a fix for the proofbox (patch | msozeau | 2009-09-08 |
* | Fix minor spelling error | glondu | 2009-08-29 |
* | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12294 85f007b7-540e-0... | fbesson | 2009-08-25 |