coq - The formal proof system

Age	Commit message (Expand)	Author
2020-10-14	Deprecating wit_var to the benefit of its synonymous wit_hyp.	Hugo Herbelin
2020-10-10	Prim.pattern_ident takes a location and its synonymous pattern_identref is de...	Hugo Herbelin
2020-09-11	[parsing] Simplify bigint	Pierre Roux
2020-09-11	[parsing] Rename token NUMERAL to NUMBER	Pierre Roux
2020-05-13	Merge PR #12229: Hopefully consensual cleaning of keywords	Théo Zimmermann
2020-05-09	Add a `with_strategy` tactic	Jason Gross
2020-05-06	Stop keeping outdated static list of keywords.	Hugo Herbelin
2020-03-22	Centralizing all kinds of numeral string management in numTok.ml.	Hugo Herbelin
2020-03-22	Adding bignat to parse positive numbers; bigint now includes negative ints.	Hugo Herbelin
2020-03-18	Merge PR #11559: Remove year in headers.	Hugo Herbelin
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-17	Dead code in g_prim.mlg	Hugo Herbelin
2020-03-03	When parsing negative integer, ensure minus sign is contiguous to the number.	Hugo Herbelin
2020-03-01	Refactor lookaheads using DSL	Maxime Dénès
2020-03-01	Move lookahead combinators to Pcoq	Maxime Dénès
2019-08-06	[parsing] unify checks for contiguity of tokens in Ltac2 and G_prim	Enrico Tassi
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-23	do not parse `\|` as infix in patterns; parse `\|}` as `\|` `}`	Georges Gonthier
2019-04-02	Add parsing of decimal constants (e.g., 1.02e+01)	Pierre Roux
2019-04-02	Rename the INT token to NUMERAL	Pierre Roux
2018-11-23	Only use Coq API in coqpp.	Pierre-Marie Pédrot
2018-07-08	Get rid of horrendous hack limiting the size of parsed integers	Maxime Dénès
2018-06-29	Port g_prim to the homebrew GEXTEND parser.	Pierre-Marie Pédrot