aboutsummaryrefslogtreecommitdiff
path: root/doc
AgeCommit message (Expand)Author
2010-07-16FSetPositive: sets of positive inspired by FMapPositive.letouzey
2010-07-08Updating reference manual credits: gb is now nsatz.herbelin
2010-06-28Update of documentation for the standard library (cf. #2332)letouzey
2010-06-26Applying François' patches about Canonical Projections (see #2302 and #2334).herbelin
2010-06-25modifs de nsatz suggerees par Hugopottier
2010-06-23Ajout d'une feuille de style pour les définitions spécifiques à Hevea + di...notin
2010-06-23Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ...notin
2010-06-18Documentation of clear dependent and revert dependentletouzey
2010-06-14Update of Extraction documentationletouzey
2010-06-14Extraction Implicit: documentationletouzey
2010-06-11Reverted commit 13110 about headers.sty that I wrongly thought was buggy. Sorry.herbelin
2010-06-10Fixed a very old (from V6.3) typo in headers.styherbelin
2010-06-08Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".herbelin
2010-06-07Backporting part of r12970 to trunk (deprecation of double induction).herbelin
2010-06-04doc Nstaz updatedpottier
2010-06-04A new command Compute foo, shortcut for Eval vm_compute in fooletouzey
2010-06-03ajout oubliepottier
2010-06-03plugin groebner updated and renamed as nsatz; first version of the doc of nsa...pottier
2010-05-28Minor fix in doc chapter on inference rules (added a missing space).herbelin
2010-05-21Extract Inductive is now possible toward non-inductive types (e.g. nat => int)letouzey
2010-05-19Remove compile-command pragmas for emacsletouzey
2010-05-18Some ocamldoc comments + Fixing name of .coqrc.version file in refmanpboutill
2010-05-09Update of credits filesherbelin
2010-05-06Correction in Function documentationjforest
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-27 small detail about Scheme Equality vsiles
2010-04-22Applying François Garillot's patch (#2261 in bug tracker) for extendedherbelin
2010-04-09Documenting the use of ##, %%, $$ in coqdoc.herbelin
2010-04-09Applied Cédric Auger's patch to fix use of "#&xxx;" in html printingherbelin
2010-03-31Add documentation on the treatment of [if] and [let (x1, ... xn) := ..]msozeau
2010-03-11Update manual on search commandspuech
2010-02-26Correction du bug #2214 + maj liens webnotin
2010-02-18Polishing the setup of CoqIDE Input Methodvgross
2010-02-11Documentation of the ! annotation for functor applicationletouzey
2010-02-10Fix [Existing Class] impl and add documentation. Fix computation of themsozeau
2010-01-30Update CHANGES, add documentation for new commands/tactics and do a bitmsozeau
2010-01-28New command Declare Reduction <id> := <conv_expr>.letouzey
2010-01-14Document Local Declare ML Moduleglondu
2010-01-07Include can accept both Module and Module Typeletouzey
2010-01-04Specific syntax for Instances in Module Type: Declare Instanceletouzey
2009-12-21Patches and instructions to enable Input Method support in CoqIDE.vgross
2009-12-15Description of the new features of the module system (part two).soubiran
2009-12-15Description of the new features of the module system (first part).soubiran
2009-11-15Document Generalizable Variables, and change syntax to msozeau
2009-11-11Added support for multiple where-clauses in Inductive and co (see wish #2163).herbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-11-04Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.gmelquio
2009-11-04Removed 'Toplevel' language from extraction documentation, since it is not cu...gmelquio
2009-11-03Report de la révision #12208 de la v8.2 (correction du bug #2126)notin
2009-11-02Correction du bug #2175notin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-10 18:18:14 +0000