coq - The formal proof system

Age	Commit message (Expand)	Author
2019-07-01	[api] Refactor most of `Decl_kinds`	Emilio Jesus Gallego Arias
2019-06-24	Move Declare to tactics folder.	Pierre-Marie Pédrot
2019-06-06	`deprecated` attribute support for notations and syntactic definitions	Maxime Dénès
2019-05-26	Move the Discharge module into the kernel.	Pierre-Marie Pédrot
2019-04-02	Add parsing of decimal constants (e.g., 1.02e+01)	Pierre Roux
2018-12-11	[api] Move reduction modules to `tactics`	Emilio Jesus Gallego Arias
2018-10-31	Fixes rest of #3468 (tactic-in-term was not respecting scopes).	Hugo Herbelin
2018-05-31	[notations] Split interpretation and parsing of notations	Emilio Jesus Gallego Arias
2018-05-31	[api] Move `Constrexpr` to the `interp` module.	Emilio Jesus Gallego Arias
2018-05-30	[api] Remove deprecated objects in engine / interp / library	Emilio Jesus Gallego Arias
2018-04-23	[api] Relocate `intf` modules according to dependency-order.	Emilio Jesus Gallego Arias
2017-11-19	[parser] Remove unnecessary statically initialized hook.	Emilio Jesus Gallego Arias
2017-11-01	[general] Move Tactypes to `interp`	Emilio Jesus Gallego Arias
2017-05-27	[coqlib] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias
2016-09-21	Merging Stdarg and Constrarg.	Pierre-Marie Pédrot
2016-01-13	Fixing #4467 (continued).	Hugo Herbelin
2014-11-27	Reverting the following block of three commits:	Hugo Herbelin
2014-11-26	Experimenting always forcing convertibility on strict implicit arguments	Hugo Herbelin
2013-12-22	Notations now accept the $(...)$ tactic-in-term syntax. They are resolved at	Pierre-Marie Pédrot
2013-06-21	Splitted up Genarg in four different levels:	ppedrot
2013-06-21	Cutting the dependency of Genarg in constr_expr, glob_constr	ppedrot
2013-06-18	Proof-of-concept: moved four easy-to-handle generic arguments to	ppedrot
2012-05-29	Avoid Dumpglob dependency on Lexer	letouzey
2012-05-29	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey
2012-05-29	Stuff about notation_constr (ex-aconstr) now in notation_ops.ml	letouzey
2011-11-21	Renamig support added to "Arguments"	gareuselesinge
2010-05-19	Nicer representation of tokens, more independant of camlp*	letouzey
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-09-11	Generalized the possibility to refer to a global name by a notation	herbelin
2009-03-20	Many changes in the Makefile infrastructure + a beginning of ocamlbuild	letouzey