coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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
\|\ \
\| * \|	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 #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
\| *	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
\|/ /
\| *	More efficient reallocation of VM global tables.	Pierre-Marie Pédrot	2018-03-26
\| *	Moving the VM global atom table to a ML reference.	Pierre-Marie Pédrot	2018-03-26
\| *	Moving the VM global data to a ML reference.	Pierre-Marie Pédrot	2018-03-26
\|/
*	Fix expected number of arguments for cumulative constructors.	Gaëtan Gilbert	2018-03-09
*	Merge PR #6775: Allow using cumulativity without forcing strict constraints.	Maxime Dénès	2018-03-09
\|\
* \	Merge PR #6769: Split closure cache and remove whd_both	Maxime Dénès	2018-03-09
\|\ \
\| \| *	Cumulativity: improve treatment of irrelevant universes.	Gaëtan Gilbert	2018-03-09
\| \| *	Allow using cumulativity without forcing strict constraints.	Gaëtan Gilbert	2018-03-09
\| \|/ \|/\|
* \|	Merge PR #6747: Relax conversion of constructors according to the pCuIC model	Maxime Dénès	2018-03-09
\|\ \
* \ \	Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values	Maxime Dénès	2018-03-09
\|\ \ \
\| * \| \|	Fix SR breakage due to allowing fixpoints on non-rec values	Matthieu Sozeau	2018-03-08
\| \| * \|	Relax conversion of constructors according to the pCuIC model	Matthieu Sozeau	2018-03-08
\| \|/ / \|/\| \|
* \| \|	Add empty description for @raise statements to satisfy ocamldoc	mrmr1993	2018-03-05
* \| \|	Replace invalid tag @raises in ocamldoc comments with @raise	mrmr1993	2018-03-05