coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-25	Separate interning and pretyping of universes	Gaëtan Gilbert
2020-10-27	Rename tactic_expr -> ltac_expr	Jim Fehrle
2020-10-14	Deprecating wit_var to the benefit of its synonymous wit_hyp.	Hugo Herbelin
2020-09-22	Fixes #9716, #13004: don't drop the qualifier of quotations at printing time.	Hugo Herbelin
2020-05-09	Add a `with_strategy` tactic	Jason Gross
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-01	Refactor lookaheads using DSL	Maxime Dénès
2020-02-22	Making structure of type "tolerability" and related clearer.	Hugo Herbelin
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-07-29	Tentatively providing a localization function to ad-hoc camlp5 parsers.	Pierre-Marie Pédrot
2019-06-19	Merge PR #10239: Deprecate grammar entry "intropattern" in tactic notations i...	Théo Zimmermann
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-06-16	Deprecate "intro_pattern" in tactic notations in favor of "simple_intropattern".	Hugo Herbelin
2019-03-20	Stop accessing proof env via Pfedit in printers	Maxime Dénès
2018-12-11	[api] Move reduction modules to `tactics`	Emilio Jesus Gallego Arias
2018-11-23	Remove the unsafe camlp5 API from the Coq codebase.	Pierre-Marie Pédrot
2018-10-15	Port remaining EXTEND ml4 files to coqpp.	Pierre-Marie Pédrot