coq - The formal proof system

Age	Commit message (Expand)	Author
2021-01-19	Remove convert_concl_no_check	Jim Fehrle
2020-11-25	Separate interning and pretyping of universes	Gaëtan Gilbert
2020-11-20	Use nat_or_var where negative values don't make sense	Jim Fehrle
2020-11-16	Merge PR #13381: Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"	coqbot-app[bot]
2020-11-15	Deprecate "eauto @int_or_var @int_or_var", add "bfs eauto"	Jim Fehrle
2020-11-15	Implement export locality for the remaining Hint commands.	Pierre-Marie Pédrot
2020-10-14	Deprecating wit_var to the benefit of its synonymous wit_hyp.	Hugo Herbelin
2020-05-25	Remove the prolog tactic.	Pierre-Marie Pédrot
2020-03-31	Try only using TC for conversion in cominductive (not great but let's see)	Gaëtan Gilbert
2020-03-18	Merge PR #11559: Remove year in headers.	Hugo Herbelin
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-18	Use a 3-valued flag for hint locality.	Pierre-Marie Pédrot
2020-03-18	Hack a non-superglobal mode for hints.	Pierre-Marie Pédrot
2020-02-28	Deprecate the "prolog" tactic.	Pierre-Marie Pédrot
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-04-30	Deprecating convert_concl_no_check.	Hugo Herbelin
2019-04-23	Deprecate the *_no_check variants of conversion tactics.	Pierre-Marie Pédrot
2019-03-27	[geninterp] Track polymorphic status in tactic interpretation.	Emilio Jesus Gallego Arias
2019-03-20	Stop accessing proof env via Pfedit in printers	Maxime Dénès
2019-02-05	Make Program a regular attribute	Maxime Dénès
2018-11-16	Remove the implicit tactic feature following #7229.	Pierre-Marie Pédrot
2018-11-02	coqpp VERNAC EXTEND uses #[ att = attribute; ] syntax	Gaëtan Gilbert
2018-11-02	Command driven attributes.	Gaëtan Gilbert
2018-11-02	Move attributes out of vernacinterp to new attributes module	Gaëtan Gilbert
2018-10-15	Port remaining EXTEND ml4 files to coqpp.	Pierre-Marie Pédrot