coq - the Coq proof assistant

	Commit message (Collapse)	Author	Age
*	Define and use UGraph.enforce_leq_alg for subtyping inference	Gaëtan Gilbert	2018-06-22
\| \| \| \|	Not sure if worth using in other places.
*	Remove enforce_leq from checker	Gaëtan Gilbert	2018-06-21
\|
*	Fix Univ.enforce_leq dropped constraints when algebraic on the right	Gaëtan Gilbert	2018-06-19
\| \| \| \| \| \| \|	There's probably a proof of false using subtyping if someone wants to look. NB: the checker doesn't handle algebraics on the right.
*	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 ↵	Enrico Tassi	2018-06-19
\|\ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	induction schemes
* \ \ \ \	Merge PR #7841: Remove Canary	Pierre-Marie Pédrot	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 ↵	Emilio Jesus Gallego Arias	2018-06-18
\|\ \ \ \ \ \ \ \ \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	example PR.
\| \| \| \| \| \| * \| \|	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.
\| \| \| \| * \| \| \|	Remove Canary.	whitequark	2018-06-18
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This eliminates 3 uses of Obj from TCB.
\| \| * \| \| \| \| \|	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 reference name type.	Maxime Dénès	2018-06-18
\| \|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
\| * \| \| \|	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
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| *	Add test-suite case for performance, had to use Timeout	Matthieu Sozeau	2018-06-15
\| \| \| \| \| \| \| \| \| \| \|
\| \| \| \| \| \| \| \| \| \| *	Better elaboration of pattern-matchings on primitive projections	Matthieu Sozeau	2018-06-15
\| \|_\|_\|_\|_\|_\|_\|_\|_\|/ \|/\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	This ensures that computations are shared as much as possible, mimicking the "positive" records computational behavior if possible.
* \| \| \| \| \| \| \| \| \|	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.