coq - The formal proof system

Age	Commit message (Expand)	Author
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-06-11	STM: encode in static types that vernac_when is only used when VtSideff	Gaëtan Gilbert
2019-06-09	[proof] Uniformize Proof_global API	Emilio Jesus Gallego Arias
2019-06-04	Alternate syntax for ![]: VERNAC EXTEND Foo STATE proof	Gaëtan Gilbert
2019-06-04	coqpp: add new ![] specifiers for structured proof interaction	Gaëtan Gilbert
2019-03-27	[coqpp] [ltac] 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-01-24	[STM] explicit handling of parsing states	Enrico Tassi
2018-11-27	Merge PR #9046: Goptions.declare_* functions return unit instead of a write_f...	Emilio Jesus Gallego Arias
2018-11-23	Remove the unsafe camlp5 API from the Coq codebase.	Pierre-Marie Pédrot
2018-11-23	s/let _ =/let () =/ in some places (mostly goptions related)	Gaëtan Gilbert
2018-11-19	Merge PR #9003: [vernacextend] Consolidate extension points API	Pierre-Marie Pédrot
2018-11-17	[vernacextend] Consolidate extension points API	Emilio Jesus Gallego Arias
2018-11-17	[ltac] Use CAst nodes in the tactic AST.	Emilio Jesus Gallego Arias
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