coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	[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
\|\ \
* \ \	Merge PR #7855: Update section on adding your project to CI and link to ↵	Emilio Jesus Gallego Arias	2018-06-18
\|\ \ \ \| \| \| \| \| \| \| \| \| \| \| \|	example PR.
\| \| * \|	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 #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 Hashcons.Hobj.	whitequark	2018-06-17
\|/ / \| \| \| \| \| \|	This eliminates 12 uses of Obj from TCB.
* \|	Merge PR #7824: Fixes #7811 (uncaught Not_found in notation printer related ↵	Pierre-Marie Pédrot	2018-06-17
\|\ \ \| \| \| \| \| \| \| \| \|	to "match").
* \ \	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
\|\ \ \ \
* \ \ \ \	Merge PR #7844: Remove Elpi from Travis.	Emilio Jesus Gallego Arias	2018-06-17
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7828: [Spawn] no control sock on unix	Emilio Jesus Gallego Arias	2018-06-17
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7818: Do not allow spliting in res_pf, this is reserved for pretyping	Pierre-Marie Pédrot	2018-06-17
\|\ \ \ \ \ \ \
\| \| \| \| \| \| \| *	Remove the proj_body field from the kernel.	Pierre-Marie Pédrot	2018-06-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This was completely wrong, such a term could not even be type-checked by the kernel as it was internally using a match construct over a negative record. They were luckily only used in upper layers, namley printing and extraction. Recomputing the projection body might be costly in detyping, but this only happens when the compatibility flag is turned on, which is not the default. Such flag is probably bound to disappear anyways. Extraction should be fixed though so as to define directly primitive projections, similarly to what has been done in native compute.
\| \| \| \| \| \| \| *	Remove the proj_eta field of the kernel.	Pierre-Marie Pédrot	2018-06-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This field was not used inside the kernel and not used in performance-critical code where caching is essential, so we extrude the code that computes it out of the kernel.
\| \| \| \| \| \| \| *	Remove special declaration of primitive projections in the kernel.	Pierre-Marie Pédrot	2018-06-17
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This reduces kernel bloat and removes code from the TCB, as compatibility projections are now retypechecked as normal definitions would have been. This should have no effect on efficiency as this only happens once at definition time.
\| \| \| \| \| \| * \|	Fixes #7811 (uncaught Not_found in notation printer related to "match").	Hugo Herbelin	2018-06-17
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
\| \| \| \| \| \| *	Getting rid of the const_proj field in the kernel.	Pierre-Marie Pédrot	2018-06-17
\| \|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This field used to signal that a constant was the compatibility eta-expansion of a primitive projections, but since a previous cleanup in the kernel it had become useless.
* \| \| \| \| \|	Merge PR #7749: [doc] Disable smartquotes conversion	Maxime Dénès	2018-06-17
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #7752: [merge script] Check if the CI that was run is outdated.	Maxime Dénès	2018-06-17
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7635: Define rec_declaration in terms of prec_declaration.	Maxime Dénès	2018-06-17
\|\ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \	Merge PR #7616: Fix #7615: Functor inlining drops universe substitution.	Maxime Dénès	2018-06-17
\|\ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \|	Remove Elpi from Travis.	Théo Zimmermann	2018-06-16
\| \|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Rather than trying to keep the version of dependencies in sync with GitLab CI.
* \| \| \| \| \| \| \| \|	Merge PR #7814: doc: Add "Print Canonical Projections" command to Command index	Théo Zimmermann	2018-06-16
\|\ \ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \| \|	[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
\|/ / / / / / / / /
\| \| \| \| \| \| * \| \|	[spawn] don't create a control socket on Unix (Fix #7713)	Enrico Tassi	2018-06-15
\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7813: Workaround for #2800: handling non-value arguments in tactics.	Pierre-Marie Pédrot	2018-06-15
\|\ \ \ \ \ \ \ \ \ \| \|_\|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \| \|
\| \| \| \| \| \| * \| \|	Do not allow spliting in res_pf, this is reserved for pretyping	Matthieu Sozeau	2018-06-15
\| \|_\|_\|_\|_\|/ / / \|/\| \| \| \| \| \| \|
\| \| \| \| \| \| * \|	cArray: proper invalid_arg exceptions	Matthieu Sozeau	2018-06-15
\| \|_\|_\|_\|_\|/ / \|/\| \| \| \| \| \|
\| * \| \| \| \| \|	Workaround to handle non-value arguments in tactics.	Cyprien Mangin	2018-06-14
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	Although the fix is not a proper one, it seems to solve every instance of #2800 that could be tested.
* \| \| \| \| \| \|	Merge PR #7803: [TYPO FIX] elimitate -> eliminate	Hugo Herbelin	2018-06-14
\|\ \ \ \ \ \ \ \| \|/ / / / / / \|/\| \| \| \| \| \|
* \| \| \| \| \| \|	Merge PR #7793: [ci] update docker image to include elpi 1.0.4	Emilio Jesus Gallego Arias	2018-06-14
\|\ \ \ \ \ \ \
* \ \ \ \ \ \ \	Merge PR #7809: Fix deprecation warning introduced by PR 664 merge	Pierre-Marie Pédrot	2018-06-14
\|\ \ \ \ \ \ \ \
\| * \| \| \| \| \| \| \|	Fix deprecation warning introduced by PR 664 merge	Matthieu Sozeau	2018-06-14
\| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \|	Merge PR #7193: Fixes #7192: Print Assumptions does not enter implementation ↵	Pierre-Marie Pédrot	2018-06-14
\|\ \ \ \ \ \ \ \ \ \| \|/ / / / / / / / \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	of submodules.
* \| \| \| \| \| \| \| \|	Merge PR #664: Fixing #5500 (missing test in return clause of match leading ↵	Matthieu Sozeau	2018-06-14
\|\ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	to anomaly)
* \ \ \ \ \ \ \ \ \	Merge PR #7787: Fixes #7780: missing lift in expanding alias under a binder ↵	Matthieu Sozeau	2018-06-14
\|\ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	in unification
* \ \ \ \ \ \ \ \ \ \	Merge PR #7105: Getting rid of some false "collision between bound variable ↵	Matthieu Sozeau	2018-06-14
\|\ \ \ \ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	names" warnings
* \ \ \ \ \ \ \ \ \ \ \	Merge PR #7771: Tweak printing boxes for unicode binders	Hugo Herbelin	2018-06-14
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| * \| \| \| \| \|	[TYPO FIX] elimitate -> eliminate	Siddharth	2018-06-14
\| \|_\|_\|_\|_\|_\|/ / / / / / \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7790: [ci] Require runner `docker` tag on `docker-boot` job.	Gaëtan Gilbert	2018-06-14
\|\ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| \| \| \| *	doc: fix typo.	whitequark	2018-06-13
\| \|_\|_\|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \|
* \| \| \| \| \| \| \| \| \| \| \|	Merge PR #7785: Document how to restart failed CI jobs.	Emilio Jesus Gallego Arias	2018-06-13
\|\ \ \ \ \ \ \ \ \ \ \ \
* \ \ \ \ \ \ \ \ \ \ \ \	Merge PR #7800: Markdown docs: switch from absolute to relative links.	Emilio Jesus Gallego Arias	2018-06-13
\|\ \ \ \ \ \ \ \ \ \ \ \ \
\| \| \| \| \| \| \| \| \| * \| \| \| \|	[ci] update docker image to include elpi 1.0.4	Enrico Tassi	2018-06-13
\| \| \| \| \| \| \| \| \| \| \| \| \| \|
\| \| * \| \| \| \| \| \| \| \| \| \| \|	Document how to restart failed CI jobs.	Théo Zimmermann	2018-06-13
\| \|/ / / / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	[ci skip]
\| * / / / / / / / / / / /	Markdown docs: switch from absolute to relative links.	Théo Zimmermann	2018-06-13
\|/ / / / / / / / / / / / \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	We had mostly used absolute links in the past. I just discovered that GitHub recommends using relative links instead: https://help.github.com/articles/basic-writing-and-formatting-syntax/#relative-links and indeed my Emacs Markdown mode can handle relative links but doesn't interpret absolute links relatively to the root of the git repository. [ci skip]