coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-30	[flags] [profile] Remove bit-rotten CProfile code.	Emilio Jesus Gallego Arias
2021-03-26	[recordops] complete API rewrite; the module is now called [structures]	Enrico Tassi
2021-02-24	Infrastructure for fine-grained debug flags	Maxime Dénès
2021-01-12	Same treatment for pattern functions used by rewrite.	Pierre-Marie Pédrot
2021-01-12	Extrude the check for pattern groundness outside of unification.	Pierre-Marie Pédrot
2021-01-04	Change the representation of kernel case.	Pierre-Marie Pédrot
2020-12-14	Do not rely on Reductionops to recognize canonical projections.	Pierre-Marie Pédrot
2020-11-23	Merge PR #13377: Fix timeout by ensuring signal exceptions are not erroneousl...	Pierre-Marie Pédrot
2020-11-22	Fix timeout by ensuring signal exceptions are not erroneously caught	Lasse Blaauwbroek
2020-11-13	Fixes #13363: case of a meta not paying attention to being under binders.	Hugo Herbelin
2020-11-05	Merge PR #13182: Check types when converting irrelevant terms in old unification	coqbot-app[bot]
2020-10-21	Introduce an Ind module in the Names API.	Pierre-Marie Pédrot
2020-10-21	Deprecate the non-qualified equality functions on kerpairs.	Pierre-Marie Pédrot
2020-10-12	Check types when converting irrelevant terms in old unification	Gaëtan Gilbert
2020-10-12	Catch more errors in Unification.abstract_list_all	Gaëtan Gilbert
2020-09-02	More efficient data structure for allowed evars	Maxime Dénès
2020-09-02	Abstract type for allowed evars	Maxime Dénès
2020-09-02	Replace `frozen` by `allowed` evars in evarconv, and delay them	Maxime Dénès
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-07-01	UIP in SProp	Gaëtan Gilbert
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-21	Merge PR #11896: Use lists instead of arrays in evar instances.	Maxime Dénès
2020-04-06	Clean and fix definitions of options.	Théo Zimmermann
2020-04-06	Use lists instead of arrays in evar instances.	Pierre-Marie Pédrot
2020-03-28	Remove some cruft from Reductionops API.	Pierre-Marie Pédrot
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-12	Remove Goptions.opt_name field	Gaëtan Gilbert
2020-02-06	unsafe_type_of -> type_of in Unification.applyHead	Gaëtan Gilbert
2020-01-06	Fix #11140: Bidirectionality hints perform (surprising?) simplification	Maxime Dénès
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-11-01	Add primitive float computation in Coq kernel	Guillaume Bertholon
2019-08-17	Delay the computation of frozen evars in legacy unification.	Pierre-Marie Pédrot
2019-07-19	Fix #10533: uncaught Invalid_argument Array.fold_left2 in rewrite	Gaëtan Gilbert
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-23	Fixing typos - Part 3	JPR
2019-05-07	Do not use the constant stack in whd_betaiota_deltazeta_for_iota_state.	Pierre-Marie Pédrot
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-02-08	Flags of evar_conv_x/unifiers: rationalize	Matthieu Sozeau
2019-02-08	Abstraction naming	Matthieu Sozeau
2019-02-08	unification: abstract_list_all_with_dependencies fix	Matthieu Sozeau
2019-02-08	[evarconv] New flag handling for unifier	Matthieu Sozeau
2019-02-08	locus: Add an AtLeastOneOccurrence constructor.	Matthieu Sozeau
2019-02-05	Make Program a regular attribute	Maxime Dénès
2019-02-04	Primitive integers	Maxime Dénès
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-11-27	Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...	Emilio Jesus Gallego Arias
2018-11-23	s/let _ =/let () =/ in some places (mostly goptions related)	Gaëtan Gilbert