coq - The formal proof system

Age	Commit message (Expand)	Author
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-05-24	Stop using pstate in global print queries	Gaëtan Gilbert
2019-05-20	Remove VtUnknown classification	Maxime Dénès
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-28	[ltac] Remove aliases already present in the lower layers.	Emilio Jesus Gallego Arias
2018-11-23	Only use Coq API in coqpp.	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	rewrite: attributes handle is_univ_poly, is_program_mode	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