coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #7080: Swapping Context and Constr and defining declarations on cons...	Maxime Dénès	2018-06-29
\|\
* \|	Deprecate Environ.retroknowledge function in favor of the projection	Gaëtan Gilbert	2018-06-28
* \|	[env.env_rel_context.env_rel_ctx] -> [rel_context env]	Gaëtan Gilbert	2018-06-28
* \|	Make Environ.globals abstract.	Gaëtan Gilbert	2018-06-28
* \|	Merge PR #7768: Fix #7723 (vm_compute segfault and proof of false)	Pierre-Marie Pédrot	2018-06-27
\|\ \
\| \| *	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin	2018-06-27
\| \|/ \|/\|
* \|	Merge PR #7863: Remove Sorts.contents	Pierre-Marie Pédrot	2018-06-27
\|\ \
\| \| *	Test file for #7723	Maxime Dénès	2018-06-27
\| \| *	Fix #7723: vm_compute segfaults with universe polymorphism	Maxime Dénès	2018-06-27
\| \|/ \|/\|
* \|	Merge PR #7919: Fix equality check on global names from native compute.	Maxime Dénès	2018-06-26
\|\ \
\| \| *	Remove Sorts.contents	Gaëtan Gilbert	2018-06-26
\| \|/ \|/\|
* \|	Merge PR #7798: Remove hack skipping comparison of algebraic universes in sub...	Matthieu Sozeau	2018-06-25
\|\ \
\| \| *	Fix equality check on global names from native compute.	Pierre-Marie Pédrot	2018-06-25
\| \|/ \|/\|
* \|	Merge PR #7772: [native_compute] Delay computations with toplevel match	Pierre-Marie Pédrot	2018-06-24
\|\ \
* \ \	Merge PR #7614: Simplify the code that handles trust of side-effects in kerne...	Maxime Dénès	2018-06-23
\|\ \ \
* \| \| \|	Adapt the kernel to generate proper data for mutual records.	Pierre-Marie Pédrot	2018-06-23
* \| \| \|	Using more general information for primitive records.	Pierre-Marie Pédrot	2018-06-23
* \| \| \|	Change the proj_ind field from MutInd.t to inductive.	Pierre-Marie Pédrot	2018-06-23
* \| \| \|	Merge PR #7715: Simplify the cooking of primitive projections.	Maxime Dénès	2018-06-23
\|\ \ \ \
* \ \ \ \	Merge PR #7600: Faster and cleaner fconstr-to-constr conversion function.	Maxime Dénès	2018-06-22
\|\ \ \ \ \
\| \| \| \| \| *	Remove hack skipping comparison of algebraic universes in subtyping.	Gaëtan Gilbert	2018-06-22
\| \| \| \| \| *	Define and use UGraph.enforce_leq_alg for subtyping inference	Gaëtan Gilbert	2018-06-22
\| \| \| \| \| *	Fix Univ.enforce_leq dropped constraints when algebraic on the right	Gaëtan Gilbert	2018-06-19
\| \|_\|_\|_\|/ \|/\| \| \| \|
* \| \| \| \|	Merge PR #7841: Remove Canary	Pierre-Marie Pédrot	2018-06-19
\|\ \ \ \ \
\| * \| \| \| \|	Remove Canary.	whitequark	2018-06-18
* \| \| \| \| \|	Remove the proj_body field from the kernel.	Pierre-Marie Pédrot	2018-06-17
* \| \| \| \| \|	Remove the proj_eta field of the kernel.	Pierre-Marie Pédrot	2018-06-17
* \| \| \| \| \|	Remove special declaration of primitive projections in the kernel.	Pierre-Marie Pédrot	2018-06-17
* \| \| \| \| \|	Getting rid of the const_proj field in the kernel.	Pierre-Marie Pédrot	2018-06-17
\|/ / / / /
\| * / / /	Faster and cleaner fconstr-to-constr conversion function.	Pierre-Marie Pédrot	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
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7677: [api] Remove Misctypes	Pierre-Marie Pédrot	2018-06-13
\|\ \ \ \ \ \
\| * \| \| \| \| \|	[api] Misctypes removal: miscellaneous aliases.	Emilio Jesus Gallego Arias	2018-06-12
* \| \| \| \| \| \|	[VM] Rename reloc -> cenv	Maxime Dénès	2018-06-12
\|/ / / / / /
\| \| \| * / /	Simplify the cooking of primitive projections.	Pierre-Marie Pédrot	2018-06-11
\| \|_\|/ / / \|/\| \| \| \|
\| \| \| \| *	[native_compute] Delay computations with toplevel match	Maxime Dénès	2018-06-11
* \| \| \| \|	[VM] Remove projection names from structured constants.	Maxime Dénès	2018-06-10
\| \|_\|_\|/ \|/\| \| \|
\| * \| \|	Fix #7615: Functor inlining drops universe substitution.	Pierre-Marie Pédrot	2018-06-07
\|/ / /
\| * \|	Define rec_declaration in terms of prec_declaration.	SimonBoulier	2018-06-05
* \| \|	More straightforward native compilation of primitive projections.	Pierre-Marie Pédrot	2018-06-05
* \| \|	Use projection indices in native compilation rather than constant names.	Pierre-Marie Pédrot	2018-06-05
\|/ /
* \|	Merge PR #7643: Fix #7631: native_compute fails to compile an example in Coq 8.8	Pierre-Marie Pédrot	2018-06-05
\|\ \
* \ \	Merge PR #7646: Fix #4714: Stack overflow with native compute	Pierre-Marie Pédrot	2018-06-05
\|\ \ \
* \ \ \	Merge PR #7495: Fix restrict_universe_context	Matthieu Sozeau	2018-06-05
\|\ \ \ \
\| \| \| * \|	Fix #7631: native_compute fails to compile an example in Coq 8.8	Maxime Dénès	2018-06-04
\| \|_\|/ / \|/\| \| \|
* \| \| \|	Merge PR #7418: Actually take advantage of the normalization status of kernel...	Maxime Dénès	2018-06-04
\|\ \ \ \
* \ \ \ \	Merge PR #7496: Fix #4403: insufficient handling of type-in-type in kernel.	Maxime Dénès	2018-06-04
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #7234: Reduce circular dependency constants <-> projections	Maxime Dénès	2018-06-01
\|\ \ \ \ \ \
\| \| \| \| \| * \|	Fix #4714: Stack overflow with native compute	Maxime Dénès	2018-05-31