coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| \| \| * \|	Inference of inductive subtyping does not need an evar map.	Gaëtan Gilbert	2018-02-10
\| \| \| * \|	Simplification: cumulativity information is variance information.	Gaëtan Gilbert	2018-02-10
\| \| \| * \|	[get_cumulativity_constraints] allowing further code sharing.	Gaëtan Gilbert	2018-02-10
\| \| \| * \|	Factorize code for comparing maybe-cumulative inductives.	Gaëtan Gilbert	2018-02-10
\| \| \| * \|	Fix typo in Univ.CumulativityInfo	Gaëtan Gilbert	2018-02-10
\| \|_\|/ / \|/\| \| \|
* \| \| \|	Merge PR #6686: Kernel/checker reduction cleanups around projection unfolding	Maxime Dénès	2018-02-07
\|\ \ \ \
\| \| \| * \|	More detailed error messages for Canonical Structure, #6398	Paul Steckler	2018-02-06
* \| \| \| \|	[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
\|\ \ \
\| \| * \|	Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-01-30
\| \|/ / \|/\| \|
* \| \|	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
\|\ \ \ \ \ \ \
\| \| \| \| \| \| \| *	Vm_compute: taking into account let-ins in parameters of constructors.	Hugo Herbelin	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