coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|/
*	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
\|/ / /
* \| \|	[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
\| * \| \| \| \|	Reduce circular dependency constants <-> projections	Gaëtan Gilbert	2018-05-31
\| \| \|_\|_\|/ \| \|/\| \| \|
* \| \| \| \|	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias	2018-05-30
* \| \| \| \|	[api] Remove deprecated aliases from `Names`.	Emilio Jesus Gallego Arias	2018-05-30
* \| \| \| \|	[api] Reintroduce `Names.global_reference` alias	Emilio Jesus Gallego Arias	2018-05-30
\|/ / / /
\| \| \| *	Fix restrict_universe_context	Gaëtan Gilbert	2018-05-30
\| \|_\|/ \|/\| \|
* \| \|	Fix #7333: vm_compute segfaults / Anomaly with cofix	Maxime Dénès	2018-05-28
* \| \|	Unify pre_env and env	Maxime Dénès	2018-05-28
* \| \|	Remove vm_conv hook and reorganize kernel files	Maxime Dénès	2018-05-28
* \| \|	Make some comments more precise about compilation of cofixpoints	Maxime Dénès	2018-05-28
* \| \|	Less confusing debug printing of setfield bytecode instruction	Maxime Dénès	2018-05-28
* \| \|	Merge pull request #7569 from ppedrot/clean-newring	Assia Mahboubi	2018-05-25
\|\ \ \
* \| \| \|	Renaming miscellaneous internal smart functions.	Hugo Herbelin	2018-05-23
* \| \| \|	Moving Rtree.smart_map into Rtree.Smart.map.	Hugo Herbelin	2018-05-23
* \| \| \|	Moving Option.smart_map to Option.Smart.map.	Hugo Herbelin	2018-05-23
* \| \| \|	Collecting List.smart_* functions into a module List.Smart.	Hugo Herbelin	2018-05-23
* \| \| \|	Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.	Hugo Herbelin	2018-05-23
* \| \| \|	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin	2018-05-23
\| * \| \|	Simplify the newring hack.	Pierre-Marie Pédrot	2018-05-21
\|/ / /
* \| \|	Merge PR #7079: Remove naked pointers from the VM	Maxime Dénès	2018-05-16
\|\ \ \
\| \| * \|	Fix #4403: insufficient handling of type-in-type in kernel.	Gaëtan Gilbert	2018-05-13
\| \|/ / \|/\| \|
* \| \|	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
\| \| *	Actually take advantage of the normalization status of kernel closures.	Pierre-Marie Pédrot	2018-05-01
\| \|/ \|/\|
\| *	Adapt the VM GC hook to handle the no-naked-pointers option flag.	Pierre-Marie Pédrot	2018-04-30
\| *	Make the VM accumulator look like an OCaml block.	Pierre-Marie Pédrot	2018-04-30
\| *	Wrap VM bytecode used on the OCaml side in an OCaml block.	Pierre-Marie Pédrot	2018-04-30
\|/
*	Merge PR #6958: [lib] Move global options to their proper place.	Maxime Dénès	2018-04-30
\|\