coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.	Maxime Dénès	2018-03-04
\|\
* \|	[VM] Unify Const_sorts and Const_type, and remove Vsort.	Maxime Dénès	2018-03-02
\| *	[econstr] Continue consolidation of EConstr API under `interp`.	Emilio Jesus Gallego Arias	2018-02-28
\|/
*	comment "resolvability" bit in Evd.evar_map	Enrico Tassi	2018-02-27
*	Merge PR #6776: Fixes bug #6774 (anomaly with ill-typed template polymorphism).	Maxime Dénès	2018-02-24
\|\
* \|	[ast] Improve precision of Ast location recognition in serialization.	Emilio Jesus Gallego Arias	2018-02-22
* \|	Merge PR #6767: [ci] add elpi	Maxime Dénès	2018-02-21
\|\ \
\| \| *	Fixes bug #6774 (anomaly with ill-typed template polymorphism).	Hugo Herbelin	2018-02-20
* \| \|	Using an "as" clause when needed for printing irrefutable patterns.	Hugo Herbelin	2018-02-20
* \| \|	Adding patterns in the category of binders for notations.	Hugo Herbelin	2018-02-20
* \| \|	Canonically add an encoding in glob_constr of "as" operator for cases_pattern.	Hugo Herbelin	2018-02-20
* \| \|	Moving the argument of CProdN/CLambdaN from binder_expr to local_binder_expr.	Hugo Herbelin	2018-02-20
\| \|/ \|/\|
\| *	pretyping: restore API understand_judgment_tcc (now understand_tcc_ty)	Enrico Tassi	2018-02-19
\|/
*	Merge PR #6759: detype_case predicate is not optional	Maxime Dénès	2018-02-19
\|\
* \|	Cleaner treatment of parameters in inferCumulativity	Gaëtan Gilbert	2018-02-16
* \|	Fix reduction flags in inferCumulativity	Gaëtan Gilbert	2018-02-16
\| *	detype_case predicate is not optional	Gaëtan Gilbert	2018-02-14
\|/
*	Merge PR #1082: Fixing Print for inductive types with let-in in parameters	Maxime Dénès	2018-02-12
\|\
* \	Merge PR #6128: Simplification: cumulativity information is variance informa...	Maxime Dénès	2018-02-12
\|\ \
* \ \	Merge PR #6418: More detailed error messages for Canonical Structure, #6398	Maxime Dénès	2018-02-12
\|\ \ \
* \ \ \	Merge PR #6651: Use r.(p) syntax to print primitive projections.	Maxime Dénès	2018-02-12
\|\ \ \ \
\| \| \| * \|	inferCumulativity: add comment to explain [if not is_arity].	Gaëtan Gilbert	2018-02-11
\| \| \| * \|	Use specialized function for inductive subtyping inference.	Gaëtan Gilbert	2018-02-11
\| \| \| * \|	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
\|\ \ \