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-25	Documenting syntax "injection ... as [= pat1 ... patn ]".	Hugo Herbelin
2019-03-27	[geninterp] Track polymorphic status in tactic interpretation.	Emilio Jesus Gallego Arias
2019-03-27	[coqpp] [ltac] Adapt to removal of imperative proof state.	Emilio Jesus Gallego Arias
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-02-05	Make Program a regular attribute	Maxime Dénès
2018-12-12	Higher-level libobject API for objects with fixed scopes	Maxime Dénès
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
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-16	Remove the implicit tactic feature following #7229.	Pierre-Marie Pédrot
2018-11-05	Merge PR #8515: Command driven attributes	Pierre-Marie Pédrot
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-30	Move abstract out of tactics.ml	Gaëtan Gilbert
2018-10-15	Port remaining EXTEND ml4 files to coqpp.	Pierre-Marie Pédrot