coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	doc: Fix markup in Calculus of Inductive Constructions	Fabian	2018-07-04
\|
*	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables
\| \| * \|	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
\| \| \| \| \| \|	I reused the sentence from the version 8.7 credits. It wasn't initially decided like this but it looks like I'm the de facto maintainer for this release as well.
*	wrong sphinx syntax	Ambroise	2018-06-28
\|
*	Update gallina-extensions.rst	Ambroise	2018-06-28
\| \| \|	I knew this feature existed but I did not remember the syntax and I could not find it in the manual
*	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
\|\ \ \
* \ \ \	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It was used in some examples, but never fully documented
\| \| \| \| *	Clarify further doc/README.md following Jim's comments.	Théo Zimmermann	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Relative links. Cf. #7800.
\| \| \| \| *	Fix copyright dates in doc/LICENSE.	Théo Zimmermann	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ci skip]
\| \| \| \| *	Improve doc/README.md.	Théo Zimmermann	2018-06-22
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	- Fix the Markdown. - Add link to latest build of the refman for the master branch. - Clarify what are the dependencies of the HTML doc. [ci skip]
\| \| \| \| *	Move INSTALL.doc into doc/README.md.	Théo Zimmermann	2018-06-22
\| \|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This will avoid in particular this ambiguous file extension. [ci skip]
* \| \| \|	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 ↵	Maxime Dénès	2018-06-21
\|\ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	understands.
* \ \ \ \ \	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We put it in a footnote otherwise the sentence was starting to be really long. Footnotes need to be in index.rst to really appear at the bottom of the index page.
\| \| \| \| \| \| *	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	It was broken and undocumented. We dropped the git logs, too, so it wasn't clear who wrote it and why it was introduced in the first place.
\| \| * \| \| \| \|	[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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	The test isn't quite the one in #7421 because that use of algebraic universes is wrong.
* \| \| \| \| \|	Fix #7829: Spurious documentation failures.	Théo Zimmermann	2018-06-18
\|/ / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We split a Require Import in two to avoid reaching the timeout.
* \| \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Move credits to its own chapter (closes #6573).
\| \| \| * \|	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
\| \|/ / \|/\| \|
* \| \|	Merge PR #7284: [sphinx] Start fixing SSR chapter.	Maxime Dénès	2018-06-11
\|\ \ \
* \ \ \	Merge PR #7515: gitlab: build sphinx doc in separate job	Emilio Jesus Gallego Arias	2018-06-09
\|\ \ \ \
\| * \| \| \|	gitlab: build sphinx doc in separate job	Gaëtan Gilbert	2018-06-08
\| \| \| \| \|
\| \| \| \| *	Existing Class noop when already a class + warning.	Gaëtan Gilbert	2018-06-08
\| \|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \|	Fix #5012.