coq - The formal proof system

Age	Commit message (Expand)	Author
2020-05-06	Stop keeping outdated static list of keywords.	Hugo Herbelin
2020-03-26	Removing deprecated destruct syntax _eqn.	Hugo Herbelin
2020-03-22	Centralizing all kinds of numeral string management in numTok.ml.	Hugo Herbelin
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-03-05	Merge PR #11522: Adding an alias `pose proof (x:=t)` for `pose proof t as x` ...	Pierre-Marie Pédrot
2020-03-03	Adding an alias "pose proof (x:=a)" for "pose proof a as x".	Hugo Herbelin
2020-03-01	[parser] lk_int -> lk_nat	Maxime Dénès
2020-03-01	Refactor lookaheads using DSL	Maxime Dénès
2019-12-05	Unfortunate bug with "cofix with": case of a CProdN over no bindings.	Hugo Herbelin
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-11-14	Rename non-unique local nonterminals	Jim Fehrle
2019-10-18	factorize or_var_map	Alexandre Moine
2019-08-19	[api] Move handling of variable implicit data to impargs	Emilio Jesus Gallego Arias
2019-07-29	Tentatively providing a localization function to ad-hoc camlp5 parsers.	Pierre-Marie Pédrot
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-04-29	Exposing a change_no_check tactic.	Hugo Herbelin
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
2019-04-01	Replace type sign = bool with SPlus \| SMinus	Pierre Roux
2019-01-23	Move and rewrite documentation for intro patterns that was under	Jim Fehrle
2018-11-23	Remove the unsafe camlp5 API from the Coq codebase.	Pierre-Marie Pédrot
2018-11-17	[ltac] Use CAst nodes in the tactic AST.	Emilio Jesus Gallego Arias
2018-09-23	[api] Deprecate constructors of deprecated datatypes.	Emilio Jesus Gallego Arias
2018-06-29	Port g_tactic to the homebrew GEXTEND parser.	Pierre-Marie Pédrot