coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-26	[recordops] complete API rewrite; the module is now called [structures]	Enrico Tassi
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-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-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	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-08	[api] Deprecate GlobRef constructors.	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
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-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-28	[ltac] Remove aliases already present in the lower layers.	Emilio Jesus Gallego Arias
2018-11-20	Merge PR #9017: Remove SSR profiling	Enrico Tassi
2018-11-17	[ltac] Use CAst nodes in the tactic AST.	Emilio Jesus Gallego Arias
2018-11-16	Remove SSR profiling	Jim Fehrle
2018-11-14	ssrmatching: unify_HO does not resolve type classes	Enrico Tassi
2018-10-30	Avoid passing dummy env to error printer	Maxime Dénès
2018-10-26	[typeclasses] functionalize typeclass evar handling	Matthieu Sozeau
2018-10-26	Cleanup evar_extra: remove evar_info's store and add maps to evar_map	Matthieu Sozeau
2018-10-15	Correct some spelling errors	Benjamin Barenblat
2018-09-19	[ssr] use the right environment in ssrpattern (fix #8454)	Enrico Tassi
2018-09-04	[ssr] anomaly -> error (Fix #8253)	Enrico Tassi