coq - The formal proof system

Age	Commit message (Expand)	Author
2020-06-18	Fix #12228 negative integers not accepted in ltac integer_list	Pierre Roux
2020-05-27	Release notes for 8.12.	Théo Zimmermann
2020-05-17	Ltac2: add notations for eval cbv in ... and other in place reductions	Michael Soegtrop
2020-05-12	Merge PR #11503: Allow to rebind the old value of a mutable Ltac2 entry.	Jason Gross
2020-05-11	Allow to rebind the old value of a mutable Ltac2 entry.	Pierre-Marie Pédrot
2020-05-08	In non-strict mode, accept any variable as a tactic reference.	Pierre-Marie Pédrot
2020-05-02	LtacProf now handles multi-success backtracking	Jason Gross
2020-04-03	Adding change log.	Hugo Herbelin
2020-03-08	Minor improvements to the unreleased changelog.	Théo Zimmermann
2020-03-03	Ltac2: Add notation for enough and eenough	Michael Soegtrop
2020-02-08	Resolve #10342 : [Ltac2] Add array library	Michael Soegtrop
2020-01-22	Changelog for 8.11.0.	Théo Zimmermann
2019-12-05	Unfortunate bug with "cofix with": case of a CProdN over no bindings.	Hugo Herbelin
2019-12-02	Move unreleased changelog to new 8.11 section.	Théo Zimmermann
2019-11-28	[changelog] Add types to changelog entries.	Théo Zimmermann
2019-10-24	Release notes for Coq 8.10.1	Vincent Laporte
2019-10-21	Adding changelog	Hugo Herbelin
2019-07-29	Document changes by PR 10324	Vincent Laporte
2019-06-08	Merge PR #10289: [Ltac2] “constr” arguments to tactic notations may have ...	Pierre-Marie Pédrot
2019-06-06	[Ltac2] Interpretation scopes in “constr” arguments of tactic notations	Vincent Laporte
2019-06-05	Changelog entry for Ltac2 (missing from #10002).	Théo Zimmermann
2019-05-05	Create categories in changelog.	Théo Zimmermann