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 #1116: Updating citing Coq in FAQ.
Maxime Dénès
2017-10-10
|
\
|
*
Updating citing Coq in FAQ.
Hugo Herbelin
2017-10-10
*
|
Fix copyright info in reference manual.
Théo Zimmermann
2017-10-06
*
|
Merge PR #1041: Miscellaneous fixes about UTF-8 (including a fix to BZ#5715 t...
Maxime Dénès
2017-10-05
|
\
\
*
\
\
Merge PR #1080: Remove some unused parts of the reference manual.
Maxime Dénès
2017-10-03
|
\
\
\
*
|
|
|
[vernac] Remove `Qed exporting` syntax.
Emilio Jesus Gallego Arias
2017-09-29
|
|
_
|
/
|
/
|
|
|
*
|
Remove some unused parts of the reference manual.
Guillaume Melquiond
2017-09-22
*
|
|
Avoid generated names for html pages of the reference manual (bug #4742).
Guillaume Melquiond
2017-09-22
|
/
/
|
*
Reference manual: A few words about the file system constraints for -Q/-R.
Hugo Herbelin
2017-09-13
|
/
*
Merge PR #1038: Fix Typo in Doc for `Set Parsing Explicit`
Maxime Dénès
2017-09-11
|
\
*
\
Merge PR #1035: Fix the introduction of SSR refman chapter.
Maxime Dénès
2017-09-11
|
\
\
*
\
\
Merge PR #1014: Add option index entry for NativeCompute Profiling
Maxime Dénès
2017-09-11
|
\
\
\
*
\
\
\
Merge PR #1004: Document primitive projections in more detail
Maxime Dénès
2017-09-11
|
\
\
\
\
|
|
|
|
*
Fix Typo in Doc for `Set Parsing Explicit`
staffehn
2017-09-08
|
|
_
|
_
|
/
|
/
|
|
|
|
|
|
*
Fix the introduction of SSR refman chapter.
Théo Zimmermann
2017-09-08
|
|
_
|
/
|
/
|
|
*
|
|
2 Typos in 'Add Parametric Morphism' Documentation
staffehn
2017-09-03
|
|
*
add option index entry for NativeCompute Profiling
Paul Steckler
2017-09-01
|
|
/
|
/
|
|
*
Document primitive projections in more detail
Matthieu Sozeau
2017-08-31
|
*
RefMan-ssr: fix warning
Matthieu Sozeau
2017-08-31
*
|
Merge PR #993: Credits for version 8.7
Maxime Dénès
2017-08-31
|
\
\
|
*
|
Credits for version 8.7
Matthieu Sozeau
2017-08-31
*
|
|
Merge PR #958: coq_makefile: build/use .cma for packed plugins too
Maxime Dénès
2017-08-31
|
\
\
\
|
|
_
|
/
|
/
|
|
|
*
|
coq_makefile: improve documentation
Enrico Tassi
2017-08-29
*
|
|
Merge PR #950: Rudimentary support for native_compute profiling, BZ#5170
Maxime Dénès
2017-08-29
|
\
\
\
*
\
\
\
Merge PR #988: Fix obsolete description of real numerals.
Maxime Dénès
2017-08-29
|
\
\
\
\
*
\
\
\
\
Merge PR #819: Cleanup old things
Maxime Dénès
2017-08-29
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #773: [flags] Remove XML output flag.
Maxime Dénès
2017-08-29
|
\
\
\
\
\
\
|
|
_
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
|
|
|
*
Update coypright dates on documentation
Matthieu Sozeau
2017-08-23
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
*
|
Fix obsolete description of real numerals.
Guillaume Melquiond
2017-08-22
|
|
_
|
/
/
|
/
|
|
|
|
|
|
*
use OCaml temp_file, instead of our own version
Paul Steckler
2017-08-18
*
|
|
|
Merge PR #973: Adding documentation for Printing Focused option.
Maxime Dénès
2017-08-18
|
\
\
\
\
|
|
|
|
*
Add native compute profiling, BZ#5170
Paul Steckler
2017-08-17
|
|
_
|
_
|
/
|
/
|
|
|
*
|
|
|
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
[next]