index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
/
refman
/
RefMan-ext.tex
Commit message (
Expand
)
Author
Age
*
Added documentation for "Set Parsing Explicit" + fixed mistakenly
herbelin
2012-01-20
*
Fixed a Not_found bug when declaring in a section some implicit
herbelin
2011-12-18
*
Command Arguments: standardizing format of error messages and American spelling.
herbelin
2011-12-17
*
Documentation of Arguments + implicits
gareuselesinge
2011-12-06
*
This adds two option tables 'Printing Record' and 'Printing Constructor'
herbelin
2011-07-16
*
This option disables the use of the '{| field := ... |}' notation
herbelin
2011-07-16
*
@ in index of refman (last request of bug 2494)
pboutill
2011-04-08
*
Fixing bug #2475 (ability to use binders in the syntax of fields was not in doc)
herbelin
2011-04-06
*
Fix formatting issue in refman
glondu
2011-01-12
*
Add "Print Sorted Universes"
glondu
2011-01-11
*
Document DOT output of universe graph
glondu
2010-11-02
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Added documentation: "Theorem id x1..xn : T" and "Set Automatic Introduction".
herbelin
2010-06-08
*
Correction in Function documentation
jforest
2010-05-06
*
Applying François Garillot's patch (#2261 in bug tracker) for extended
herbelin
2010-04-22
*
Document Generalizable Variables, and change syntax to
msozeau
2009-11-15
*
Fixed record syntax "{|x=...; y=...|}" so that it works with qualified names.
gmelquio
2009-11-04
*
Fixed some typos in the reference manual.
gmelquio
2009-10-29
*
- Fixed various Overfull in documentation.
herbelin
2009-01-27
*
Last changes in type class syntax:
msozeau
2009-01-18
*
- Standardized prefix use of "Local"/"Global" modifiers as decided in
herbelin
2009-01-13
*
Lissage de la gestion des chemins de chargement de fichiers :
herbelin
2008-06-29
*
Modif un peu gadget (??): on peut écrire "set (f n:=t)" pour
herbelin
2008-04-26
*
- Un peu de doc, préparation du CHANGES pour la release.
herbelin
2008-04-15
*
Fix examples in Program documentation and add comindexes for the various
msozeau
2008-03-23
*
Fix the clrewrite tactic, change Relations.v to work on relations in Prop
msozeau
2008-02-09
*
Documentation of CHANGES and refman doc for the implicit argument binder
msozeau
2008-02-08
*
- Documentation des nouvelles options d'implicites (Set Strongly Strict
herbelin
2008-02-06
*
Unification de TacLetRecIn et TacLetIn. En particulier, on peut
herbelin
2008-02-01
*
Finish let| implementation and document it
msozeau
2008-01-31
*
Standardisation du format des références croisées vers Figure, Section, Ch...
herbelin
2008-01-05
*
Ajout possibilité d'options à trois mots.
herbelin
2007-04-29
*
Fixed some typos.
glondu
2007-04-18
*
Changed many refman/*.tex files. Put \label and \index commands that immediat...
emakarov
2007-04-17
*
Cleaned doc/common/title.tex file. Increased the space under headers
emakarov
2007-04-12
*
Meilleur anglais (cf 9619)
herbelin
2007-02-07
*
Relecture/nettoyage chapitre Gallina; déplacement section Function
herbelin
2007-02-07
*
Documentation de "Set Printing Universes", "Print Universes" (anciennement
herbelin
2006-10-28
*
Documentation Declare Implicit Tactic, Print Canonical Projections, ... + lé...
herbelin
2006-07-07
*
Documentation or-pattern
herbelin
2006-07-04
*
Nettoyage de l'archive doc et restructuration avant intégration à l'archive
herbelin
2006-02-23