coq - The formal proof system

Age	Commit message (Expand)	Author
2020-04-10	[ocamlformat] Enable for funind.	Emilio Jesus Gallego Arias
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-07-31	[funind] Remove export of `generate_functional_principle` and `make_scheme`	Emilio Jesus Gallego Arias
2019-07-15	[funind] Remove unneeded callback.	Emilio Jesus Gallego Arias
2019-06-24	Duplicate the type of constant entries in Proof_global.	Pierre-Marie Pédrot
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-06-11	Remove the side-effect role from the kernel.	Pierre-Marie Pédrot
2018-06-18	Remove reference name type.	Maxime Dénès
2018-02-27	Update headers following #6543.	Théo Zimmermann
2018-01-24	Remove dead code from funind.	Maxime Dénès
2017-11-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
2017-09-08	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert
2017-07-17	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-16	Removing Proof_type from the API.	Pierre-Marie Pédrot
2017-06-10	Remove (useless) aliases from the API.	Matej Košík
2017-06-07	Put all plugins behind an "API".	Matej Kosik
2017-02-14	Funind API using EConstr.	Pierre-Marie Pédrot
2016-01-20	Update copyright headers.	Maxime Dénès
2015-10-28	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi
2015-04-14	Function now supports puniveres	jforest
2012-12-14	Modulification of identifier	ppedrot
2012-05-29	locus.mli for occurrences+clauses, misctypes.mli for various little things	letouzey
2010-12-24	More {raw => glob} changes for consistency	glondu
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2009-09-17	Delete trailing whitespaces in all .{v,ml} files	glondu
2009-03-20	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey