coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
\| * \| \|	kernel: cleanup projection unfolding	Gaëtan Gilbert	2018-02-02
\|/ / /
\| * /	Use whd-all on rigid-flex conversion.	Pierre-Marie Pédrot	2018-02-02
\|/ /
* \|	Merge PR #6666: Fix reduction of primitive projections on coinductive records...	Maxime Dénès	2018-01-30
\|\ \
* \ \	Merge PR #6649: Fix #6621: Anomaly on fixpoint with primitive projections	Maxime Dénès	2018-01-30
\|\ \ \
\| \| * \|	[native_compute] Fix evaluation of cofixpoints under primitive projections.	Maxime Dénès	2018-01-29
* \| \| \|	Safer VM interfaces	Maxime Dénès	2018-01-26
\| \|/ / \|/\| \|
\| * \|	Fix #6621: Anomaly on fixpoint with primitive projections	Maxime Dénès	2018-01-24
\|/ /
* \|	Merge PR #6627: Fix #6619: coqchk does not reduce compatibility constants for...	Maxime Dénès	2018-01-23
\|\ \
* \ \	Merge PR #6506: Fast rel lookup	Maxime Dénès	2018-01-22
\|\ \ \
\| \| * \|	Remove dead code in Environ.	Pierre-Marie Pédrot	2018-01-20
\| \|/ / \|/\| \|
* \| \|	Store the conversion oracle in constant and inductive definitions.	Pierre-Marie Pédrot	2018-01-14
* \| \|	Merge PR #6578: Remove references to deleted Unicode.Unsupported exception	Maxime Dénès	2018-01-13
\|\ \ \
* \| \| \|	Enforce that polymorphic definitions do not generate internal constraints.	Pierre-Marie Pédrot	2018-01-11
\| * \| \|	Remove references to removed Unicode.Unsupported	Jasper Hugunin	2018-01-11
\|/ / /
* \| \|	Add a comment about universe lifting in sections in the kernel.	Pierre-Marie Pédrot	2017-12-31
* \| \|	Moving some universe substitution code out of the kernel.	Pierre-Marie Pédrot	2017-12-30
* \| \|	Returning instance instead of substitution in universe context abstraction.	Pierre-Marie Pédrot	2017-12-30
* \| \|	Hardening universe abstraction in Cooking.	Pierre-Marie Pédrot	2017-12-30
\| * \|	Share the rel environment between Environ.env and reduction cache.	Pierre-Marie Pédrot	2017-12-29
\| * \|	Fast environment lookup for rels.	Pierre-Marie Pédrot	2017-12-29
\|/ /
* \|	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
* \|	Merge PR #6469: No universe constraints in Let definitions	Maxime Dénès	2017-12-22
\|\ \
* \ \	Merge PR #6449: Let definitions must not contain side-effects when reaching t...	Maxime Dénès	2017-12-20
\|\ \ \
\| \| * \|	Let definitions do not create new universe constraints.	Pierre-Marie Pédrot	2017-12-19
\| \| * \|	Specific type for section definition entries.	Pierre-Marie Pédrot	2017-12-19
\| \|/ /
* \| \|	Fix order of let-in representation comment.	Jasper Hugunin	2017-12-19
\| * \|	Let definitions must not contain side-effects when reaching the kernel.	Pierre-Marie Pédrot	2017-12-16
\|/ /
* \|	Merge PR #6264: [kernel] Patch allowing to disable VM reduction.	Maxime Dénès	2017-12-14
\|\ \
\| \| *	Cosmetic: using "types" rather "constr" in some types of term.mli.	Hugo Herbelin	2017-12-14
\| \| *	Fixing a bug of Print for inductive types with let-ins in parameters.	Hugo Herbelin	2017-12-14
\| \| *	Fixes incorrect anomaly message in lambda/prod_applist_assum + typo in doc.	Hugo Herbelin	2017-12-14
* \| \|	Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.	Maxime Dénès	2017-12-14
\|\ \ \ \| \|_\|/ \|/\| \|
* \| \|	Merge PR #6368: [api] Remove yet another type alias.	Maxime Dénès	2017-12-11
\|\ \ \
* \| \| \|	[api] Remove kernel dependency on intf (Decl_kind)	Emilio Jesus Gallego Arias	2017-12-10
\| * \| \|	[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
\|/ /
\| *	[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
\|/
*	Fix native compute for byte compiled Coq.	Gaëtan Gilbert	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
\| *	When declaring constants/inductives use ContextSet if monomorphic.	Gaëtan Gilbert	2017-11-24
\|/
*	Merge PR #486: Make some functions on terms more robust w.r.t new term constr...	Maxime Dénès	2017-11-24
\|\
\| *	Make some functions on terms more robust w.r.t new term constructs.	Maxime Dénès	2017-11-23
* \|	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias	2017-11-22
* \|	[api] Miscellaneous consolidation + moves to engine.	Emilio Jesus Gallego Arias	2017-11-21
\|/
*	Merge PR #6058: Remove redundant env argument to Reduction.ccnv	Maxime Dénès	2017-11-15
\|\
* \|	[ci] [coq] Complete 4.06.0 support.	Emilio Jesus Gallego Arias	2017-11-13
* \|	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
* \|	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias	2017-11-06