coq - The formal proof system

Age	Commit message (Expand)	Author
2020-10-21	Introduce an Ind module in the Names API.	Pierre-Marie Pédrot
2020-04-06	Clean and fix definitions of options.	Théo Zimmermann
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-02-12	Remove Goptions.opt_name field	Gaëtan Gilbert
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2018-12-12	[rtauto] [auto] Use new proof engine.	Emilio Jesus Gallego Arias
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-11-23	s/let _ =/let () =/ in some places (mostly goptions related)	Gaëtan Gilbert
2018-10-18	[universes] deprecate constr_of_global	Matthieu Sozeau
2018-10-10	[coqlib] Rebindable Coqlib namespace.	Emilio Jesus Gallego Arias
2018-05-17	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-11-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
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-10	Remove (useless) aliases from the API.	Matej Košík
2017-06-07	Put all plugins behind an "API".	Matej Kosik
2017-05-27	[coqlib] Deprecate redundant Coqlib functions.	Emilio Jesus Gallego Arias
2017-05-24	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias
2017-04-13	Silence a few OCaml warnings.	Guillaume Melquiond
2017-03-24	Merge branch 'trunk' into pr379	Maxime Dénès
2017-02-17	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot
2017-02-14	Definining EConstr-based contexts.	Pierre-Marie Pédrot
2017-02-14	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot
2017-02-14	Tactics API using EConstr.	Pierre-Marie Pédrot
2017-02-14	Retyping API using EConstr.	Pierre-Marie Pédrot
2017-02-14	Termops API using EConstr.	Pierre-Marie Pédrot
2016-08-19	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias
2016-08-19	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias
2016-07-03	closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)	Pierre Letouzey
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey
2016-07-01	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès
2016-05-31	Feedback cleanup	Emilio Jesus Gallego Arias
2016-05-16	Put the "exact" family of tactic in the monad.	Pierre-Marie Pédrot
2016-02-09	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik
2016-01-20	Update copyright headers.	Maxime Dénès
2015-01-12	Update headers.	Maxime Dénès
2014-06-12	Passing some tactics to the new monad type.	Pierre-Marie Pédrot
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-12	Term.dest* functions now raise specific DestKO exn instead of Invalid_argument	letouzey
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-08-08	Updating headers.	herbelin
2012-07-05	ZArith + other : favor the use of modern names instead of compat notations	letouzey
2012-06-01	Getting rid of Pp.msgnl and Pp.message.	ppedrot
2012-03-02	Noise for nothing	pboutill
2011-11-24	Fixed some missing options from previous commit.	ppedrot