coq - The formal proof system

Age	Commit message (Expand)	Author
2020-03-01	[parser] lk_int -> lk_nat	Maxime Dénès
2020-03-01	Refactor lookaheads using DSL	Maxime Dénès
2020-03-01	Move lookahead combinators to Pcoq	Maxime Dénès
2020-02-25	Merge PR #11655: [parsing] Track need to reinit by typing	Pierre-Marie Pédrot
2020-02-24	Merge PR #11560: Fix #11549: Ltac2 is incompatible with $.	Tej Chajed
2020-02-21	[parsing] Track need to reinit by typing	Emilio Jesus Gallego Arias
2020-02-19	Fix #11549: Ltac2 is incompatible with $.	Pierre-Marie Pédrot
2020-02-19	Fix #11552: Ltac2 breaks query commands during proofs.	Pierre-Marie Pédrot
2019-11-14	Rename non-unique local nonterminals	Jim Fehrle
2019-11-06	Swap parsing precedence of `::` and `,` ; Fix #10116	Kenji Maillard
2019-10-29	Fix #10615: Notation substitution for Ltac2 terms.	Pierre-Marie Pédrot
2019-10-18	Allow to pass Ltac1 values to Ltac2 quotations.	Pierre-Marie Pédrot
2019-08-06	[parsing] unify checks for contiguity of tokens in Ltac2 and G_prim	Enrico Tassi
2019-07-29	Fix #10088: Incompatibility with ssreflect's ampersand syntactic sugar.	Pierre-Marie Pédrot
2019-07-29	Tentatively providing a localization function to ad-hoc camlp5 parsers.	Pierre-Marie Pédrot
2019-06-25	Adding the ability to transfer Ltac2 variables to Ltac1 quotations.	Pierre-Marie Pédrot
2019-06-17	Update headers of files that were stuck on older headers.	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	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