coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding	Maxime Dénès	2018-02-07
\|\
* \|	[native_compute] Fix handling of evars in conversion	Maxime Dénès	2018-02-05
* \|	[native_compute] Remove useless conversion to list in reification.	Maxime Dénès	2018-02-05
\| *	Reductionops.nf_* now take an environment.	Gaëtan Gilbert	2018-02-02
\|/
*	Merge PR #6535: Cleanup name-binding structure for fresh evar name generation.	Maxime Dénès	2018-01-31
\|\
* \	Merge PR #6666: Fix reduction of primitive projections on coinductive records...	Maxime Dénès	2018-01-30
\|\ \
\| * \|	[cbv] Fix evaluation of cofixpoints under primitive projections.	Maxime Dénès	2018-01-29
* \| \|	Safer VM interfaces	Maxime Dénès	2018-01-26
\|/ /
* \|	Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for...	Maxime Dénès	2018-01-23
\|\ \
\| * \|	Remove dead code in Environ.	Pierre-Marie Pédrot	2018-01-20
* \| \|	Fix context handling of fix and cofix in Ltac subterm matching.	Cyprien Mangin	2018-01-19
* \| \|	Define EConstr version of [push_rec_types].	Cyprien Mangin	2018-01-19
\|/ /
\| *	Cleanup name-binding structure for fresh evar name generation.	Pierre-Marie Pédrot	2018-01-02
* \|	Moving some universe substitution code out of the kernel.	Pierre-Marie Pédrot	2017-12-30
* \|	Using a dedicated type for Lib.abstr_info.	Pierre-Marie Pédrot	2017-12-30
\|/
*	Remove the local polymorphic flag hack.	Maxime Dénès	2017-12-27
*	Merge PR #6439: [api] Also deprecate constructors of Decl_kinds.	Maxime Dénès	2017-12-27
\|\
* \	Merge PR #6289: Remove unused boolean from cl_context field of Typeclasses.ty...	Maxime Dénès	2017-12-27
\|\ \
\| \| *	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
\| \|/ \|/\|
* \|	Merge PR #6436: Fix #5368: Canonical structure unification fails.	Maxime Dénès	2017-12-18
\|\ \
* \ \	Merge PR #6392: [econstr] Cleanup in `vernac/classes.ml`	Maxime Dénès	2017-12-15
\|\ \ \
\| \| * \|	Fix #5368: Canonical structure unification fails.	Pierre-Marie Pédrot	2017-12-15
\| \|/ / \|/\| \|
* \| \|	Merge PR #6264: [kernel] Patch allowing to disable VM reduction.	Maxime Dénès	2017-12-14
\|\ \ \
* \ \ \	Merge PR #978: In printing, experimenting factorizing "match" clauses with sa...	Maxime Dénès	2017-12-14
\|\ \ \ \
* \ \ \ \	Merge PR #6373: Further clean-up in Reductionops, removing unused lift argume...	Maxime Dénès	2017-12-14
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6169: Clean up/deprecated options	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \
* \ \ \ \ \ \	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \ \ \ \ \ \
\| \| \| \| \| \| * \|	[econstr] Cleanup in `vernac/classes.ml`.	Emilio Jesus Gallego Arias	2017-12-13
\| \| \| \| * \| \| \|	Decompiling pattern-matching: mini-removal dead code.	Hugo Herbelin	2017-12-12
\| \| \| \| * \| \| \|	In printing, factorizing "match" clauses with same right-hand side.	Hugo Herbelin	2017-12-12
\| \| \| \| * \| \| \|	Removing cumbersome location in multiple patterns.	Hugo Herbelin	2017-12-12
\| \| \| * \| \| \| \|	Further clean-up in Reductionops, removing unused lift arguments.	Maxime Dénès	2017-12-12
\| \| \| \| \|_\|/ / \| \| \| \|/\| \| \|
* \| \| / \| \| \|	[proof] Embed evar_map in RefinerError exception.	Emilio Jesus Gallego Arias	2017-12-11
\| \|_\|/ / / / \|/\| \| \| \| \|
\| \| * \| \| \|	Remove deprecated option Tactic Compat Context.	Théo Zimmermann	2017-12-11
\| \|/ / / / \|/\| \| \| \|
* \| \| \| \|	Merge PR #6368: [api] Remove yet another type alias.	Maxime Dénès	2017-12-11
\|\ \ \ \ \
* \ \ \ \ \	Merge PR #6338: Remove up-to-conversion term matching	Maxime Dénès	2017-12-11
\|\ \ \ \ \ \ \| \|_\|_\|/ / / \|/\| \| \| \| \|
\| \| * \| \| \|	[api] Remove yet another type alias.	Emilio Jesus Gallego Arias	2017-12-09
\| \|/ / / / \|/\| \| \| \|
\| \| * \| \|	[lib] Rename Profile to CProfile	Emilio Jesus Gallego Arias	2017-12-09
\| \|/ / / \|/\| \| \|
\| * \| \|	Remove up-to-conversion matching functions.	Pierre-Marie Pédrot	2017-12-09
* \| \| \|	Getting rid of the Update constructor in Reductionops.	Pierre-Marie Pédrot	2017-12-06
* \| \| \|	Getting rid of the Shift constructor in Reductionops.	Pierre-Marie Pédrot	2017-12-06
\|/ / /
\| * \|	[kernel] Patch allowing to disable VM reduction.	Emilio Jesus Gallego Arias	2017-12-02
* \| \|	Proper nametab handling of global universe names	Matthieu Sozeau	2017-12-01
\|/ /
* \|	Merge PR #6274: Attempt to fix inversion disregarding singleton types (fixes ...	Maxime Dénès	2017-11-30
\|\ \
\| \| *	Remove unused boolean from cl_context field of Typeclasses.typeclass	Gaëtan Gilbert	2017-11-30
\| \|/ \|/\|
\| *	Adding a variant get_truncation_family_of of get_sort_family_of.	Hugo Herbelin	2017-11-28
\| *	Moving non-recursive function sort_family_of out of the retype block of recur...	Hugo Herbelin	2017-11-28
* \|	Merge PR #1033: Universe binder improvements	Maxime Dénès	2017-11-28
\|\ \
* \| \|	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias	2017-11-26
\| \|/ \|/\|
\| *	Fix interpretation of global universes in univdecl constraints.	Gaëtan Gilbert	2017-11-25