index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
/
refman
Commit message (
Expand
)
Author
Age
*
Merge PR #973: Adding documentation for Printing Focused option.
Maxime Dénès
2017-08-18
|
\
*
\
Merge PR #974: Change section caption, improve some wording
Maxime Dénès
2017-08-17
|
\
\
*
|
|
Document anonymous universes (PR #544).
Gaëtan Gilbert
2017-08-17
|
|
*
Adding documentation for Printing Focused option.
Pierre Courtieu
2017-08-17
|
|
/
|
/
|
|
*
mention that tactic is the identity or gives error
Paul Steckler
2017-08-16
|
*
change section caption, improve some wording
Paul Steckler
2017-08-16
|
/
*
Merge PR #831: Port ssreflect user manual to Coq's latex/hevea style
Maxime Dénès
2017-08-16
|
\
*
\
Merge PR #948: [doc] Write (@nil nat) instead of (nil nat)
Maxime Dénès
2017-08-16
|
\
\
*
\
\
Merge PR #943: Reference Manual: minor wording improvements
Maxime Dénès
2017-08-16
|
\
\
\
*
\
\
\
Merge PR #934: Fix some coq-tex errors in the reference manual.
Maxime Dénès
2017-08-16
|
\
\
\
\
*
\
\
\
\
Merge PR #864: Some cleanups after cumulativity for inductive types
Maxime Dénès
2017-08-16
|
\
\
\
\
\
|
|
|
|
|
*
Rewording the introduction
Enrico Tassi
2017-08-02
|
|
|
|
|
*
Rephrasing a couple of sentences in a more factual way.
Hugo Herbelin
2017-08-02
|
|
|
|
|
*
Rephrasing the introduction in a more factual and up-to-date way.
Hugo Herbelin
2017-08-02
|
|
|
|
|
*
Port ssr manual to Coq's latex/hevea style
Enrico Tassi
2017-08-02
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
*
Update Setoid.tex
larsr
2017-08-02
|
|
_
|
_
|
/
|
/
|
|
|
|
*
|
|
Typo in the documentation of cumulativity
Amin Timany
2017-08-02
*
|
|
|
Merge PR #933: Fix documentation of Hint Mode (bug #4911).
Maxime Dénès
2017-08-01
|
\
\
\
\
*
\
\
\
\
Merge PR #932: Fix shuffled documentation.
Maxime Dénès
2017-08-01
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #929: Add missing paragraph to introduction
Maxime Dénès
2017-08-01
|
\
\
\
\
\
\
*
\
\
\
\
\
\
Merge PR #925: Document Extraction TestCompile
Maxime Dénès
2017-08-01
|
\
\
\
\
\
\
\
*
\
\
\
\
\
\
\
Merge PR #775: [toplevel] Remove long ago deprecated and NOOP options.
Maxime Dénès
2017-08-01
|
\
\
\
\
\
\
\
\
|
|
|
|
|
|
|
|
*
Fix incorrect use of "At the end".
Sam Pablo Kuper
2017-07-31
|
|
|
|
|
|
|
|
*
Minor grammar fix: replace a "then" with a "so".
Sam Pablo Kuper
2017-07-31
|
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
*
|
Update documentation of cumulativity
Amin Timany
2017-07-31
|
|
|
|
|
|
*
|
Fix typo and Add Jason's example to the doc
Amin Timany
2017-07-31
|
|
|
|
|
|
*
|
Improve documentation of cumulativity
Amin Timany
2017-07-31
|
|
_
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
*
|
|
|
Drop paragraph mentioning Addendum as separate doc.
Théo Zimmermann
2017-07-29
*
|
|
|
|
|
|
Merge PR #823: Async off in Windows by default in CoqIDE
Maxime Dénès
2017-07-28
|
\
\
\
\
\
\
\
|
|
|
|
|
|
|
*
Fix some coq-tex errors in the reference manual.
Guillaume Melquiond
2017-07-28
|
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
*
Fix documentation of Hint Mode (bug #4911).
Guillaume Melquiond
2017-07-28
|
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
*
Fix shuffled documentation.
Guillaume Melquiond
2017-07-28
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
*
Add missing paragraph to introduction
Benjamin Pierce
2017-07-27
|
|
_
|
_
|
/
|
/
|
|
|
|
|
|
*
Extraction.tex: mention the possible "From Coq Require Extraction"
letouzey
2017-07-27
|
|
|
*
Extraction TestCompile documented + mentionned in CHANGES
Pierre Letouzey
2017-07-27
|
|
_
|
/
|
/
|
|
|
|
*
[toplevel] Remove long ago deprecated and NOOP options.
Emilio Jesus Gallego Arias
2017-07-27
|
|
/
|
/
|
*
|
Merge branch 'v8.7'
Maxime Dénès
2017-07-20
|
\
\
|
*
\
Merge PR #745: Add timing scripts
Maxime Dénès
2017-07-19
|
|
\
\
*
|
\
\
Merge PR #865: RefMan-ext: fix some typos
Maxime Dénès
2017-07-17
|
\
\
\
\
|
*
|
|
|
Update with non structurally recursive
william-lawvere
2017-07-14
|
|
*
|
|
Sync the manual with the deprecation warnings.
Théo Zimmermann
2017-07-11
|
|
/
/
/
|
/
|
|
|
|
|
*
|
Document the timing targets
Jason Gross
2017-07-11
|
|
*
|
Strip trailing spaces
Jason Gross
2017-07-11
|
|
/
/
|
/
|
|
|
*
|
RefMan-ext: fix some typos
William Lawvere
2017-07-07
*
|
|
Merge PR #835: Remove doc/refman/RefMan-ind.tex
Maxime Dénès
2017-07-07
|
\
\
\
|
|
/
/
|
/
|
|
*
|
|
Merge PR #837: Add inversion_sigma to CHANGES and to doc
Maxime Dénès
2017-07-05
|
\
\
\
*
\
\
\
Merge PR #850: Improve grammar in RefMan-Gal and RefMan-syn
Maxime Dénès
2017-07-05
|
\
\
\
\
*
\
\
\
\
Merge PR #832: Document an example `Makefile` for `coq_makefile`
Maxime Dénès
2017-07-05
|
\
\
\
\
\
*
\
\
\
\
\
Merge branch 'v8.6'
Pierre-Marie Pédrot
2017-07-04
|
\
\
\
\
\
\
|
|
|
*
|
|
|
Update RefMan-syn.tex
william-lawvere
2017-07-01
[next]