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
...
*
Several bug reports came from confusions between generalize and set.
pboutill
2011-09-01
*
Bug 2583: Update of the syntax of terms in the reference manual
pboutill
2011-09-01
*
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
*
coq_makefile documentation in Refman and -h
pboutill
2011-07-07
*
doc/stdlib: Update the list of ZArith files
letouzey
2011-07-04
*
update of Micromega doc
fbesson
2011-06-29
*
refman nsatz
pottier
2011-06-16
*
update of the file list in doc/stdlib
letouzey
2011-05-06
*
Adding "Tactic Notation" in doc index.
herbelin
2011-04-28
*
Documentation typo.
gmelquio
2011-04-15
*
Add directories in COQPATH to search path.
herbelin
2011-04-14
*
remove old traces of SearchIsos (never ported to 7.x nor 8.x)
letouzey
2011-04-12
*
@ 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
*
Add 'Existing Instances' declaration to declare multiple instances at once.
letouzey
2011-04-06
*
Update documentation concerning proofs loading (cf last commit)
letouzey
2011-04-03
*
Documentation of the timeout tactical (cf r13917)
letouzey
2011-03-21
*
An option "Set Default Timeout n."
letouzey
2011-03-17
*
Restore documentation of library String which was removed in 2007 (r10049)
herbelin
2011-03-05
*
Remove obsolete TheoryList
glondu
2011-02-10
*
Fix formatting issue in refman
glondu
2011-01-12
*
Remove references to -ide option of coqmktop
glondu
2011-01-11
*
Add "Print Sorted Universes"
glondu
2011-01-11
*
Precision in documentation of "decide equality"
glondu
2010-12-24
*
Remove the two-argument variant of "decide equality"
glondu
2010-12-23
*
More precise documentation for instantiate
glondu
2010-12-23
*
Example of a simple ML tactic (Hello world).
fkirchne
2010-12-09
*
Numbers and bitwise functions.
letouzey
2010-12-06
*
Applied patch to FAQ proposed by Hendrik Tews (bug report #2446).
herbelin
2010-12-04
*
Documentation for tactic constr_eq
glondu
2010-12-02
*
Add tactic has_evar (#2433)
glondu
2010-12-02
*
Add tactic is_evar (Closes: #2433)
glondu
2010-12-02
*
SearchAbout: who has never been annoyed by the [ ] syntax ?
letouzey
2010-11-19
*
Integer division: quot and rem (trunc convention) in addition to div and mod
letouzey
2010-11-10
*
Numbers: axiomatization, properties and implementations of gcd
letouzey
2010-11-05
*
Fix typo in "Hint Extern" doc
glondu
2010-11-03
*
Document DOT output of universe graph
glondu
2010-11-02
*
Numbers : log2. Abstraction, properties and implementations.
letouzey
2010-11-02
*
Move stuff about positive into a distinct PArith subdir
letouzey
2010-11-02
*
More precise description of boolean ring in doc (see bug #2401)
glondu
2010-10-11
*
TeX input method is now supported upstream
vgross
2010-10-07
*
Remove Explain* vernacs
glondu
2010-10-06
*
Remove VernacGo
glondu
2010-10-06
*
(Hopefully) clearer explanation of Ltac's context patterns
glondu
2010-10-05
*
Added multiple implicit arguments rules per name.
herbelin
2010-10-03
*
Minor fixes of 'make doc'
pboutill
2010-09-28
*
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
[prev]
[next]