coq - The formal proof system

Age	Commit message (Expand)	Author
2021-01-18	Merge PR #13454: Remove unused retro_refl	Pierre-Marie Pédrot
2021-01-04	Remove redundant univ and parameter info from CaseInvert	Gaëtan Gilbert
2021-01-04	Change the representation of kernel case.	Pierre-Marie Pédrot
2020-12-09	Optimization: take advantage that we don't use arrays anymore in substitutions.	Pierre-Marie Pédrot
2020-11-23	Remove unused retro_refl	Gaëtan Gilbert
2020-11-21	Rename the confusing neutral annotation in CClosure.	Pierre-Marie Pédrot
2020-11-13	Remove unused CClosure.FNativeEntries.farray	Gaëtan Gilbert
2020-11-03	Add a fast path in CClosure stack zipping.	Pierre-Marie Pédrot
2020-10-26	Yet another normal / neutral bug in primitive conversion.	Pierre-Marie Pédrot
2020-10-26	Fix bug in conversion of primitive values.	Pierre-Marie Pédrot
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-04-03	Be cleverer and do not hopelessly rezip a term when not needed.	Pierre-Marie Pédrot
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
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-07-25	Mark primitives integer as able to participate in reductions (fixes #10560).	Guillaume Melquiond
2019-07-16	Move unfold_side_flags CClosure -> Tacred internals	Gaëtan Gilbert
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-23	Fixing typos - Part 2	JPR
2019-05-19	Make the type of constant bodies parametric on opaque proofs.	Pierre-Marie Pédrot
2019-03-14	Put [@inline] on CClosure.Mark functions	Gaëtan Gilbert
2019-03-14	mutable relevance marks in fconstr	Gaëtan Gilbert
2019-03-14	Enable proof irrelevance for SProp.	Gaëtan Gilbert
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-02-04	Primitive integers	Maxime Dénès
2018-12-23	Remove dead code from CClosure.	Pierre-Marie Pédrot
2018-11-20	Use a closure for the domain argument of FProd.	Pierre-Marie Pédrot
2018-11-20	Do not wrap FProd return types in a closure.	Pierre-Marie Pédrot
2018-11-19	Rename TranspState into TransparentState.	Pierre-Marie Pédrot
2018-11-19	Proper record type and accessors for transparent states.	Pierre-Marie Pédrot
2018-11-19	Move transparent_state to its own module.	Pierre-Marie Pédrot
2018-10-31	Merge PR #8752: Enable fragile pattern warning in cclosure	Maxime Dénès
2018-10-17	Enable fragile pattern warning in cclosure	Gaëtan Gilbert
2018-10-11	Clean up CClosure code.	Pierre-Marie Pédrot
2018-10-11	The cbv reduction does not rely on the kernel info data structure anymore.	Pierre-Marie Pédrot
2018-10-04	Remove FCast from CClosure.fterm.	Pierre-Marie Pédrot
2018-09-26	Inline the definition of CClosure.mk_clos_deep.	Pierre-Marie Pédrot
2018-09-24	[kernel] Compile with almost all warnings enabled.	Emilio Jesus Gallego Arias
2018-07-26	Turn the kernel reduction sharing flag into an argument passed in the cache.	Pierre-Marie Pédrot
2018-07-24	Projections use index representation	Gaëtan Gilbert
2018-06-27	Swapping Context and Constr: defining declarations on constr in Constr.	Hugo Herbelin
2018-06-23	Using more general information for primitive records.	Pierre-Marie Pédrot
2018-06-17	Faster and cleaner fconstr-to-constr conversion function.	Pierre-Marie Pédrot
2018-06-04	Merge PR #7418: Actually take advantage of the normalization status of kernel...	Maxime Dénès
2018-05-28	Unify pre_env and env	Maxime Dénès
2018-05-23	Exporting Fun1 within Array so that Array.Fun1 and not only CArray.Fun1 works.	Hugo Herbelin