coq - The formal proof system

Age	Commit message (Expand)	Author
2020-07-24	Fixes reduction effect printing in the presence of non purely applicative sta...	Hugo Herbelin
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-07-01	UIP in SProp	Gaëtan Gilbert
2020-04-06	Use lists instead of arrays in evar instances.	Pierre-Marie Pédrot
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-02-12	Remove Goptions.opt_name field	Gaëtan Gilbert
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-11-01	Implement classify on primitive float	Pierre Roux
2019-11-01	Change return type of primitive float comparison	Pierre Roux
2019-11-01	Add primitive float computation in Coq kernel	Guillaume Bertholon
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-23	Fixing typos - Part 3	JPR
2019-05-19	Make the type of constant bodies parametric on opaque proofs.	Pierre-Marie Pédrot
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-02-04	Primitive integers	Maxime Dénès
2018-11-28	[options] New helper for creation of boolean options plus reference.	Emilio Jesus Gallego Arias
2018-11-23	s/let _ =/let () =/ in some places (mostly goptions related)	Gaëtan Gilbert
2018-10-11	The cbv reduction does not rely on the kernel info data structure anymore.	Pierre-Marie Pédrot
2018-09-23	Checking if low-level name printers are used on purpose or not.	Hugo Herbelin
2018-07-26	Turn the kernel reduction sharing flag into an argument passed in the cache.	Pierre-Marie Pédrot
2018-07-25	Merge PR #7889: Cleanup reduction effects: they only work on constants.	Pierre-Marie Pédrot
2018-07-24	Projections use index representation	Gaëtan Gilbert
2018-07-12	Cleanup reduction effects: they only work on constants.	Gaëtan Gilbert
2018-03-28	[api] Deprecate a couple of aliases that we missed.	Emilio Jesus Gallego Arias
2018-03-09	Merge PR #6769: Split closure cache and remove whd_both	Maxime Dénès
2018-03-04	Pass the constant cache as a separate argument in kernel reduction.	Pierre-Marie Pédrot
2018-02-27	Update headers following #6543.	Théo Zimmermann
2018-01-29	[cbv] Fix evaluation of cofixpoints under primitive projections.	Maxime Dénès
2017-11-26	[api] Remove aliases of `Evar.t`	Emilio Jesus Gallego Arias
2017-11-15	Fix #5761: cbv on undefined evars under binders produces unbound rel	Gaëtan Gilbert
2017-11-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-04	Added support for a side effect on constants in reduction functions.	Thomas Sibut-Pinote
2017-05-24	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias
2017-05-03	Added an option Set Debug Cbv.	Hugo Herbelin
2017-02-14	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot
2017-02-14	Cbv API using EConstr.	Pierre-Marie Pédrot
2016-07-03	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey
2016-07-01	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès
2016-04-29	Fix incorrect cbv reduction of primitive projections. (Bug #4634)	Guillaume Melquiond
2016-01-20	Update copyright headers.	Maxime Dénès
2015-01-12	Update headers.	Maxime Dénès
2014-12-09	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey
2014-10-15	To stay closer to non-primitive projections, only unfold primitive	Matthieu Sozeau
2014-09-27	Fix bug 3662 by actually reducing primitive projections in cbv/compute.	Matthieu Sozeau
2014-09-27	Add a boolean to indicate the unfolding state of a primitive projection,	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2012-12-18	Modulification of name	ppedrot
2012-11-22	Monomorphization (pretyping)	ppedrot