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 #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
|
\
\
*
|
|
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 #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
[next]