coq - The formal proof system

Age	Commit message (Expand)	Author
2021-03-10	Allow to register deprecation status in Ltac2 term and notation declarations.	Pierre-Marie Pédrot
2020-10-27	Rename tac2type -> ltac2_type,	Jim Fehrle
2020-10-26	Ltac2: use ComTactic infrastructure	Gaëtan Gilbert
2020-04-15	[declare] Rename `Declare.t` to `Declare.Proof.t`	Emilio Jesus Gallego Arias
2020-04-15	[proof] Merge `Proof_global` into `Declare`	Emilio Jesus Gallego Arias
2020-03-25	[pcoq] Inline the exported Gramlib interface instead of exposing it as G	Emilio Jesus Gallego Arias
2020-03-25	[parsing] Remove extend AST in favor of gramlib constructors	Emilio Jesus Gallego Arias
2020-03-25	[parsing] Make grammar extension type private.	Emilio Jesus Gallego Arias
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-10-18	Allow to pass Ltac1 values to Ltac2 quotations.	Pierre-Marie Pédrot
2019-06-17	Update headers of files that were stuck on older headers.	Théo Zimmermann
2019-06-04	Rename Proof_global.{pstate -> t}	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-05-07	Integrate build and documentation of Ltac2	Maxime Dénès