coq - The formal proof system

Age	Commit message (Expand)	Author
2021-01-26	[vernac] Check that no proofs do remain open at section/module closing time	Emilio Jesus Gallego Arias
2020-10-15	Support "Solve Obligations of <ident>" option	Jim Fehrle
2020-10-04	Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."	Jim Fehrle
2020-09-11	Turn integer into natural in several mlgs	Pierre Roux
2020-07-08	[obligations] Functionalize Program state	Emilio Jesus Gallego Arias
2020-06-26	[declare] Merge remaining obligations bits into Declare	Emilio Jesus Gallego Arias
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-08-29	Make sure that all query commands return a notice (not an info) feedback	Maxime Dénès
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-06-11	STM: encode in static types that vernac_when is only used when VtSideff	Gaëtan Gilbert
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-06-04	Proof_global: pass only 1 pstate when we don't want the proof stack	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-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-11-23	Remove the unsafe camlp5 API from the Coq codebase.	Pierre-Marie Pédrot
2018-11-17	[vernacextend] Consolidate extension points API	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