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 #8028: Fix a few typos
Théo Zimmermann
2018-07-10
|
\
*
\
Merge PR #8025: Fix rst syntax for `quote ident {ident}`
Théo Zimmermann
2018-07-10
|
\
\
|
|
*
Fix typo in doc/proof-engine/tactics.rst.
whitequark
2018-07-10
|
|
/
|
/
|
*
|
Merge PR #7920: Generic syntax for attributes
Maxime Dénès
2018-07-09
|
\
\
|
|
*
Fix rst syntax for `quote ident {ident}`
Joachim Breitner
2018-07-09
|
|
/
|
/
|
*
|
Remove Emacs modes.
Théo Zimmermann
2018-07-08
*
|
Merge PR #7921: Archive the `gallina` tool
Maxime Dénès
2018-07-07
|
\
\
*
|
|
doc: Fix markup in Calculus of Inductive Constructions
Fabian
2018-07-04
|
|
*
Describe attributes in the documentation.
Vincent Laporte
2018-07-03
|
|
/
|
/
|
*
|
Merge PR #7820: [hints] Add Hint Variables/Constants Opaque/Transparent commands
Pierre-Marie Pédrot
2018-07-03
|
\
\
*
\
\
Merge PR #7703: Add an option to force parameters to be uniform
Matthieu Sozeau
2018-07-02
|
\
\
\
*
\
\
\
Merge PR #7969: doc: typesetting and hyperlinks in Syntax Extensions
Théo Zimmermann
2018-07-02
|
\
\
\
\
|
|
|
*
|
hints: add Hint Variables/Constants Opaque/Transparent commands
Matthieu Sozeau
2018-07-02
|
|
*
|
|
Document option Uniform Inductive Parameters
Jasper Hugunin
2018-07-01
|
|
|
/
/
|
*
/
/
doc: typesetting and hyperlinks in Syntax Extensions
Lysxia
2018-06-30
|
|
/
/
*
/
/
doc: Fix typesetting in Gallina extensions
Lysxia
2018-06-29
|
/
/
*
|
Self-credit for the work done.
Théo Zimmermann
2018-06-28
*
|
wrong sphinx syntax
Ambroise
2018-06-28
*
|
Update gallina-extensions.rst
Ambroise
2018-06-28
*
|
Merge PR #7866: Implementation of mutual records in the higher strata
Maxime Dénès
2018-06-28
|
\
\
*
\
\
Merge PR #7783: Move INSTALL.doc to doc/README.md and improve a few things.
Maxime Dénès
2018-06-26
|
\
\
\
*
\
\
\
Merge PR #7851: Modernize the introduction of the reference manual.
Maxime Dénès
2018-06-26
|
\
\
\
\
|
|
|
|
*
Archive the `gallina` tool
Vincent Laporte
2018-06-25
|
|
_
|
_
|
/
|
/
|
|
|
*
|
|
|
Merge PR #7559: Existing Class noop when already a class + warning.
Matthieu Sozeau
2018-06-25
|
\
\
\
\
|
|
|
|
*
Documenting the syntax of mutual keywords.
Pierre-Marie Pédrot
2018-06-24
|
|
_
|
_
|
/
|
/
|
|
|
*
|
|
|
Merge PR #7784: Remove Tutorials from a few other places following #7466.
Maxime Dénès
2018-06-24
|
\
\
\
\
*
|
|
|
|
[ssr] document {}/view
Enrico Tassi
2018-06-22
*
|
|
|
|
[ssr] document rewrite {}foo
Enrico Tassi
2018-06-22
|
|
|
|
*
Clarify further doc/README.md following Jim's comments.
Théo Zimmermann
2018-06-22
|
|
|
|
*
Fix copyright dates in doc/LICENSE.
Théo Zimmermann
2018-06-22
|
|
|
|
*
Improve doc/README.md.
Théo Zimmermann
2018-06-22
|
|
|
|
*
Move INSTALL.doc into doc/README.md.
Théo Zimmermann
2018-06-22
|
|
_
|
_
|
/
|
/
|
|
|
*
|
|
|
Merge PR #7770: Move indices on top on the TOC. Closes #7764.
Maxime Dénès
2018-06-21
|
\
\
\
\
*
\
\
\
\
Merge PR #7815: On cygwin, pass the filename in a format that coqdoc understa...
Maxime Dénès
2018-06-21
|
\
\
\
\
\
*
\
\
\
\
\
Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.
Maxime Dénès
2018-06-21
|
\
\
\
\
\
\
|
|
|
|
|
|
*
Mention Company-Coq as well.
Théo Zimmermann
2018-06-20
|
|
|
|
|
|
*
Add a good reference for Proof-General as suggested by Clément.
Théo Zimmermann
2018-06-20
|
|
|
|
|
|
*
Modernize the introduction of the reference manual.
Théo Zimmermann
2018-06-20
|
|
_
|
_
|
_
|
_
|
/
|
/
|
|
|
|
|
|
|
*
|
|
|
On cygwin, pass the filename in a format that coqdoc understands.
Jim Fehrle
2018-06-20
*
|
|
|
|
|
Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.
Pierre-Marie Pédrot
2018-06-19
|
\
\
\
\
\
\
|
|
*
|
|
|
|
[doc] Rewrite and document the prodn directive
Clément Pit-Claudel
2018-06-19
|
|
*
|
|
|
|
[doc] Fix a typo in the ssreflect chapter
Clément Pit-Claudel
2018-06-19
|
|
*
|
|
|
|
[doc] Fix uncaught duplicate-label errors in the SSReflect chapter
Clément Pit-Claudel
2018-06-19
|
|
*
|
|
|
|
[doc] Use productionlist instead of prodn in ring.rst
Clément Pit-Claudel
2018-06-19
|
|
/
/
/
/
/
|
/
|
|
|
|
|
|
*
|
|
|
|
Fix #7421: constr_eq ignores universe constraints.
Gaëtan Gilbert
2018-06-18
*
|
|
|
|
|
Fix #7829: Spurious documentation failures.
Théo Zimmermann
2018-06-18
|
/
/
/
/
/
*
|
|
|
|
Merge PR #7848: Fix a typo in documentation
Théo Zimmermann
2018-06-17
|
\
\
\
\
\
|
|
|
|
*
|
Remove Tutorial from Additional documentation in refman intro.
Théo Zimmermann
2018-06-17
|
|
|
|
*
|
Remove Tutorials from doc/LICENSE following #7466.
Théo Zimmermann
2018-06-17
|
|
_
|
_
|
/
/
|
/
|
|
|
|
|
|
|
*
|
Add introduction and credits to the TOC.
Théo Zimmermann
2018-06-17
[next]