coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
*	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
\|\
* \	Merge PR #6892: Cleanup implementation of normalize_context_set a bit	Pierre-Marie Pédrot	2018-04-28
\|\ \
* \| \|	Always print explanation for univ inconsistency, rm Flags.univ_print	Gaëtan Gilbert	2018-04-26
* \| \|	Merge PR #6908: Move VM global tables from C to ML	Maxime Dénès	2018-04-20
\|\ \ \
\| \| * \|	universe normalisation: put equivalence class partition in UGraph	Gaëtan Gilbert	2018-04-13
\| \|/ / \|/\| \|
* \| \|	Merge PR #6972: [api] Deprecate a couple of aliases that we missed.	Maxime Dénès	2018-04-12
\|\ \ \
* \ \ \	Merge PR #7176: Fix #6956: Uncaught exception in bytecode compilation	Pierre-Marie Pédrot	2018-04-09
\|\ \ \ \
\| * \| \| \|	Fix #6956: Uncaught exception in bytecode compilation	Maxime Dénès	2018-04-06
\| \| \| \| *	[lib] Move global options to their proper place.	Emilio Jesus Gallego Arias	2018-04-02
\| \| \|_\|/ \| \|/\| \|
\| \| * \|	[api] Deprecate a couple of aliases that we missed.	Emilio Jesus Gallego Arias	2018-03-28
\| \|/ /
* / /	Expliciting and taking advantage of a representation invariant in Esubst.	Pierre-Marie Pédrot	2018-03-27
\|/ /