index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
doc
/
sphinx
Commit message (
Expand
)
Author
Age
*
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 #7851: Modernize the introduction of the reference manual.
Maxime Dénès
2018-06-26
|
\
\
*
\
\
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
*
|
|
|
Merge PR #7770: Move indices on top on the TOC. Closes #7764.
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
|
|
_
|
_
|
_
|
/
|
/
|
|
|
|
*
|
|
|
|
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
|
|
_
|
/
/
|
/
|
|
|
|
|
*
|
Add introduction and credits to the TOC.
Théo Zimmermann
2018-06-17
|
|
*
|
Move indexes on top on the TOC. Closes #7764.
Théo Zimmermann
2018-06-17
|
|
/
/
|
/
|
|
*
|
|
Merge PR #7749: [doc] Disable smartquotes conversion
Maxime Dénès
2018-06-17
|
\
\
\
*
|
|
|
[sphinx] Finish clean-up of the Canonical Structure subsection.
Théo Zimmermann
2018-06-16
*
|
|
|
doc: Add "Print Canonical Projections" command to Command index
Anton Trunov
2018-06-16
|
|
*
|
doc: fix typo.
whitequark
2018-06-13
|
|
/
/
|
/
|
|
|
|
*
Existing Class noop when already a class + warning.
Gaëtan Gilbert
2018-06-08
|
*
|
[doc] Disable smartquotes conversion
Clément Pit-Claudel
2018-06-08
|
|
/
*
|
Improve links to SSR tactics, and some other improvements.
Théo Zimmermann
2018-06-05
*
|
Workaround a weird error of .. coqtop::
Théo Zimmermann
2018-06-05
*
|
Remove many abusive .. coqtop in SSR chapter.
Théo Zimmermann
2018-06-05
*
|
A few additional small fixes.
Théo Zimmermann
2018-06-05
*
|
[sphinx] Fix missing indices warnings.
Théo Zimmermann
2018-06-05
*
|
[ssr] index entry for "without loss", "suffices" and "generally have"
Enrico Tassi
2018-06-05
*
|
[ssr] some fixes to the documentation markup
Enrico Tassi
2018-06-05
*
|
[sphinx] Start fixing SSR chapter.
Théo Zimmermann
2018-06-05
|
/
*
Merge PR #7229: Deprecate implicit tactic solving.
Hugo Herbelin
2018-06-04
|
\
*
\
Merge PR #7481: document 7025 (coq_makefile flag variables)
Maxime Dénès
2018-06-04
|
\
\
[next]