coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7774: [build] Fix checks and notes noting 4.02.1 instead of 4.02.3	Maxime Dénès	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7873: Make Clément the secondary codeowner of doc/tools/coqrst.	Maxime Dénès	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Update dpdgraph branch name	Gaëtan Gilbert	2018-06-21
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7770: Move indices on top on the TOC. Closes #7764.	Maxime Dénès	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|/ / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Further cleanup: do not export the closed_term Ltac entry.	Pierre-Marie Pédrot	2018-06-21
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7815: On cygwin, pass the filename in a format that coqdoc understa...	Maxime Dénès	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| *	Inline a function from Quote used in setoid_ring.	Pierre-Marie Pédrot	2018-06-21
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7865: Fix #7432: Grammar token @term points to the SSR chapter.	Maxime Dénès	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \|	Remove enforce_leq from checker	Gaëtan Gilbert	2018-06-21
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7842: Fix #7836: tools/inferior-coq.el uses next-line instead of fo...	Pierre Courtieu	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7880: Clean up Dyn	Pierre-Marie Pédrot	2018-06-21
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Add documentation for Dyn.	whitequark	2018-06-21
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Rename Dyn.TParam→ValueS, Dyn.MapS.obj→value to clarify their purpose.	whitequark	2018-06-21
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Reformat Dyn.{ml,mli}.	whitequark	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 #7868: [coqtop] Give priority to stdlib load path over current direc...	Emilio Jesus Gallego Arias	2018-06-20
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	[ssr] test case for rewrite (setoid) making the goal illtyped	Enrico Tassi	2018-06-20
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \| \| \|	[ssr] rewrite: turn anomaly into regular error	Enrico Tassi	2018-06-20
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \|	Make Clément the secondary codeowner of doc/tools/coqrst.	Théo Zimmermann	2018-06-20
\| \|_\|_\|_\|_\|/ / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| * \| \|	Fix Univ.enforce_leq dropped constraints when algebraic on the right	Gaëtan Gilbert	2018-06-19
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[coqtop] Give priority to stdlib load path over current directory	Maxime Dénès	2018-06-19
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7797: Remove reference name type.	Enrico Tassi	2018-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #6754: Better elaboration of pattern-matchings on primitive projections	Pierre-Marie Pédrot	2018-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7491: Fix #7421: constr_eq ignores universe constraints.	Pierre-Marie Pédrot	2018-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7801: [vernac] Add option to force building really mutual induction...	Enrico Tassi	2018-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7841: Remove Canary	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
\| \|_\|_\|_\|_\|_\|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7714: Remove primitive-projection related data from the kernel	Maxime Dénès	2018-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7856: Fix #7829: Spurious documentation failures.	Maxime Dénès	2018-06-19
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Overlay for reference removal	Maxime Dénès	2018-06-18
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7855: Update section on adding your project to CI and link to examp...	Emilio Jesus Gallego Arias	2018-06-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix #7421: constr_eq ignores universe constraints.	Gaëtan Gilbert	2018-06-18
\| \|_\|_\|_\|_\|/ / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Remove Canary.	whitequark	2018-06-18
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Fix #7829: Spurious documentation failures.	Théo Zimmermann	2018-06-18
\| \| \| \|/ / / / / / / / / / / / / / / / / \| \| \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7840: Remove Hashcons.Hobj	Pierre-Marie Pédrot	2018-06-18
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \| \|_\|/ / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Update section on adding your project to CI and link to example PR.	Théo Zimmermann	2018-06-18
\| \|/ / / / / / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| * \| \| \| \| \| \| \| \| \| \| \| \| \|	Remove reference name type.	Maxime Dénès	2018-06-18
\| \|_\|_\|_\|/ / / / / / / / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| * \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Remove Hashcons.Hobj.	whitequark	2018-06-17
\|/ / / / / / / / / / / / / / / / /
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7824: Fixes #7811 (uncaught Not_found in notation printer related t...	Pierre-Marie Pédrot	2018-06-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7848: Fix a typo in documentation	Théo Zimmermann	2018-06-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7822: cArray: proper invalid_arg exceptions	Pierre-Marie Pédrot	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
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7844: Remove Elpi from Travis.	Emilio Jesus Gallego Arias	2018-06-17
\|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \