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
*
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 #940: Replace jarring use of "Remark" with "Note"
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
|
|
|
|
|
|
*
Makefile.doc: implement serve-refman-8080 target
Enrico Tassi
2017-08-02
|
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
*
Update Setoid.tex
larsr
2017-08-02
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
*
|
|
|
Typo in the documentation of cumulativity
Amin Timany
2017-08-02
|
|
|
*
|
Improve style slightly
Sam Pablo Kuper
2017-08-01
*
|
|
|
|
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
|
|
_
|
_
|
_
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
*
Replace jarring use of "Remark" with "Note"
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
|
|
/
|
/
|
*
|
Adding a V8.7 compatibility version number.
Hugo Herbelin
2017-07-21
*
|
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 #842: Update the Tutorial.
Maxime Dénès
2017-07-07
|
\
\
\
[next]
Maxime Dénès
Gaëtan Gilbert
Pierre Courtieu
Paul Steckler
Enrico Tassi
Hugo Herbelin
larsr
Amin Timany
Sam Pablo Kuper
Théo Zimmermann
Guillaume Melquiond
Benjamin Pierce
letouzey
Emilio Jesus Gallego Arias
william-lawvere
Jason Gross