index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
Commit message (
Expand
)
Author
Age
*
Added a section in the documentation of Vernacular commands about Set/Unset/T...
aspiwack
2010-09-23
*
Hopefully a fix for #2176 (redirection not understood with some shells)
herbelin
2010-09-19
*
Added doc/refman/coqide.eps and coqide-queries.eps to remove the need for png...
emakarov
2010-09-06
*
unification des tactiques nsatz pour R Z avec celle des anneaux integres
pottier
2010-07-28
*
Minor fixes:
msozeau
2010-07-27
*
Documentation of Set Automatic Coercions Import.
herbelin
2010-07-25
*
Extension of the recursive notations mechanism
herbelin
2010-07-22
*
FSetPositive: sets of positive inspired by FMapPositive.
letouzey
2010-07-16
*
Updating reference manual credits: gb is now nsatz.
herbelin
2010-07-08
*
Update of documentation for the standard library (cf. #2332)
letouzey
2010-06-28
*
Applying François' patches about Canonical Projections (see #2302 and #2334).
herbelin
2010-06-26
*
modifs de nsatz suggerees par Hugo
pottier
2010-06-25
*
Ajout d'une feuille de style pour les définitions spécifiques à Hevea + di...
notin
2010-06-23
*
Mise à jour des liens au site Coq (suite à la MAJ de la redirection DNS de ...
notin
2010-06-23
*
Documentation of clear dependent and revert dependent
letouzey
2010-06-18
*
Update of Extraction documentation
letouzey
2010-06-14
*
Extraction Implicit: documentation
letouzey
2010-06-14
*
Reverted commit 13110 about headers.sty that I wrongly thought was buggy. Sorry.
herbelin
2010-06-11
*
Fixed a very old (from V6.3) typo in headers.sty
herbelin
2010-06-10
*
Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".
herbelin
2010-06-08
*
Backporting part of r12970 to trunk (deprecation of double induction).
herbelin
2010-06-07
*
doc Nstaz updated
pottier
2010-06-04
*
A new command Compute foo, shortcut for Eval vm_compute in foo
letouzey
2010-06-04
*
ajout oublie
pottier
2010-06-03
*
plugin groebner updated and renamed as nsatz; first version of the doc of nsa...
pottier
2010-06-03
*
Minor fix in doc chapter on inference rules (added a missing space).
herbelin
2010-05-28
*
Extract Inductive is now possible toward non-inductive types (e.g. nat => int)
letouzey
2010-05-21
*
Remove compile-command pragmas for emacs
letouzey
2010-05-19
*
Some ocamldoc comments + Fixing name of .coqrc.version file in refman
pboutill
2010-05-18
*
Update of credits files
herbelin
2010-05-09
*
Correction in Function documentation
jforest
2010-05-06
*
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
[next]