coq - The formal proof system

Age	Commit message (Expand)	Author
2020-07-05	Further cleanup of dead code in the Reductionops API.	Pierre-Marie Pédrot
2020-07-05	Inline the Reductionops.fix_recarg function.	Pierre-Marie Pédrot
2020-07-01	UIP in SProp	Gaëtan Gilbert
2020-06-04	Further cleanup.	Pierre-Marie Pédrot
2020-06-04	Move the cbn reduction to its own file, and simplify the RAKAM accordingly.	Pierre-Marie Pédrot
2020-05-10	Further cleanup: remove the local_reduction_function type.	Pierre-Marie Pédrot
2020-05-10	No more local reduction functions in Reductionops.	Pierre-Marie Pédrot
2020-04-06	Clean and fix definitions of options.	Théo Zimmermann
2020-04-03	Be cleverer and do not hopelessly rezip a term when not needed.	Pierre-Marie Pédrot
2020-04-03	Use the kernel machine in whd_betaiota_deltazeta_for_iota_state.	Pierre-Marie Pédrot
2020-03-31	Merge PR #11889: Fix a spelling mistake in the code: s/magicaly/magically/	Enrico Tassi
2020-03-28	Remove some cruft from Reductionops API.	Pierre-Marie Pédrot
2020-03-23	s/magicaly/magically/	Jason Gross
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-03	[exninfo] Deprecate aliases for exception re-raising.	Emilio Jesus Gallego Arias
2020-02-25	Fix backtraces in conversion anomalies caught by Reductionops.	Pierre-Marie Pédrot
2020-02-14	Use thunks to univ instead of lazy constr for template typing	Gaëtan Gilbert
2020-02-12	Remove Goptions.opt_name field	Gaëtan Gilbert
2020-02-09	Fix #11553: magicaly_constant_of_fixbody checks existence of made up constant	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-08-29	Fix a few wrong uses of `msg_notice`	Maxime Dénès
2019-07-08	[api] Deprecate GlobRef constructors.	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-23	Fixing typos - Part 3	JPR
2019-05-10	Remove various circumvolutions from reduction behaviors	Maxime Dénès
2019-05-07	Do not use the constant stack in whd_betaiota_deltazeta_for_iota_state.	Pierre-Marie Pédrot
2019-04-08	Don't store closures in summary (reduction effects)	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-12	Higher-level libobject API for objects with fixed scopes	Maxime Dénès
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-11-23	s/let _ =/let () =/ in some places (mostly goptions related)	Gaëtan Gilbert
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-11-06	Move debug term printer to kernel	Maxime Dénès
2018-10-30	Avoid redefining reduction functions in fun_ind	Maxime Dénès
2018-10-20	Cleanup comparing projections through their constants.	Gaëtan Gilbert
2018-10-05	[kernel] Remove section paths from `KerName.t`	Maxime Dénès
2018-09-26	[print] Restrict use of "debug" Termops printer.	Emilio Jesus Gallego Arias
2018-09-23	Checking if low-level name printers are used on purpose or not.	Hugo Herbelin
2018-09-12	Move maps & sets indexed by GlobRef.t into the kernel	Vincent Laporte
2018-09-06	Fixing #8270 (cbn was calling zeta even when not asked for).	Hugo Herbelin
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-06-04	Stronger invariants in unification signature.	Pierre-Marie Pédrot