coq - The formal proof system

Age	Commit message (Expand)	Author
2021-04-23	Relying on the abstract notion of streams with location for parsing.	Hugo Herbelin
2021-03-26	[recordops] complete API rewrite; the module is now called [structures]	Enrico Tassi
2021-03-03	[build] Split stdlib to it's own opam package.	Emilio Jesus Gallego Arias
2021-01-04	Change the representation of kernel case.	Pierre-Marie Pédrot
2020-12-27	Refactor cpattern into a record	Lasse Blaauwbroek
2020-12-27	Make ssrtermkind algebraic instead of a char	Lasse Blaauwbroek
2020-12-18	Make ssr datastructures cpattern and rpattern public	Lasse Blaauwbroek
2020-11-25	Separate interning and pretyping of universes	Gaëtan Gilbert
2020-11-19	Use a proper canonical structure entry for projections.	Hugo Herbelin
2020-10-21	Deprecate the non-qualified equality functions on kerpairs.	Pierre-Marie Pédrot
2020-10-11	Similarly remove the explicit graph argument in the ~evar conversion API.	Pierre-Marie Pédrot
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-07-03	Fix #11121: Simultaneous definition of term and notation in custom grammar	Maxime Dénès
2020-07-01	UIP in SProp	Gaëtan Gilbert
2020-05-22	Merge PR #12295: Fixes #12233: printing environment corrupted with eta-expans...	Pierre-Marie Pédrot
2020-05-13	Ssrmatching: Hack to circumvent a hack.	Hugo Herbelin
2020-05-10	No more local reduction functions in Reductionops.	Pierre-Marie Pédrot
2020-05-03	Remove legacy SSR API.	Pierre-Marie Pédrot
2020-05-03	Further SSR port.	Pierre-Marie Pédrot
2020-05-03	Remove legacy layer in SSR.	Pierre-Marie Pédrot
2020-05-03	Wrap ssr tactics into V82.tactic.	Pierre-Marie Pédrot
2020-04-21	Merge PR #11896: Use lists instead of arrays in evar instances.	Maxime Dénès
2020-04-11	[dune] [stdlib] Build the standard library natively with Dune.	Emilio Jesus Gallego Arias
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-19	Addressing #6082 and #7766 (overriding format of notation).	Hugo Herbelin
2020-02-13	[build] Consolidate stdlib's .v files under a single directory.	Emilio Jesus Gallego Arias
2020-02-13	Merge PR #11521: Remove Goptions.opt_name field	Pierre-Marie Pédrot
2020-02-12	Remove Goptions.opt_name field	Gaëtan Gilbert
2020-02-12	Standardize constr -> globref operations to use destRef/isRef/isRefX	Gaëtan Gilbert
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-19	[api] Move handling of variable implicit data to impargs	Emilio Jesus Gallego Arias
2019-07-29	Tentatively providing a localization function to ad-hoc camlp5 parsers.	Pierre-Marie Pédrot
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 2	JPR
2019-05-13	Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.	Hugo Herbelin
2019-05-13	Moving Evd.evars_of_term from constr to econstr + consequences.	Hugo Herbelin
2019-05-10	Make the check flag of conversion functions mandatory.	Pierre-Marie Pédrot
2019-03-27	[geninterp] Track polymorphic status in tactic interpretation.	Emilio Jesus Gallego Arias
2019-03-27	[plugins] [ssr] Adapt to removal of imperative proof state.	Emilio Jesus Gallego Arias
2019-03-20	Stop accessing proof env via Pfedit in printers	Maxime Dénès
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-02-08	Change interfaces of evarconv as suggested by Enrico.	Matthieu Sozeau
2019-02-06	Fix #9281: forgotten CeCILL-B headers in ssrmatching plugin.	Théo Zimmermann
2019-02-04	Primitive integers	Maxime Dénès
2018-12-25	[ssrmatching] update license banner (fix #9281)	Enrico Tassi
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-11-28	[ltac] Remove aliases already present in the lower layers.	Emilio Jesus Gallego Arias