coq - The formal proof system

Age	Commit message (Expand)	Author
2020-11-25	Separate interning and pretyping of universes	Gaëtan Gilbert
2020-10-29	Fixing interpretation of rewrite_strat argument in Ltac.	Hugo Herbelin
2020-10-14	Deprecating wit_var to the benefit of its synonymous wit_hyp.	Hugo Herbelin
2020-10-04	Remove prefixes on nonterminal names, e.g. "constr:" and "Prim."	Jim Fehrle
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-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	[rewrite] Add Morphism syntax made different for module type parameters	Enrico Tassi
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