coq - The formal proof system

Age	Commit message (Expand)	Author
2020-10-21	Rename the GlobRef comparison modules following the standard pattern.	Pierre-Marie Pédrot
2020-06-19	Wrap the content of full hints into a record.	Pierre-Marie Pédrot
2020-06-19	Opacify the type of hint metadata.	Pierre-Marie Pédrot
2020-05-10	No more local reduction functions in Reductionops.	Pierre-Marie Pédrot
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-02-12	Standardize constr -> globref operations to use destRef/isRef/isRefX	Gaëtan Gilbert
2020-02-06	unsafe_type_of -> type_of in Sequent.extend_with_auto_hints	Gaëtan Gilbert
2019-12-06	Moving the diversity of constr printers to a label style.	Hugo Herbelin
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-04-10	Remove calls to global env in Inductiveops	Maxime Dénès
2019-03-20	Stop accessing proof env via Pfedit in printers	Maxime Dénès
2018-09-12	Move maps & sets indexed by GlobRef.t into the kernel	Vincent Laporte
2018-05-25	Remove some occurrences of Evd.empty	Maxime Dénès
2018-05-04	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias
2018-04-13	Evar maps contain econstrs.	Gaëtan Gilbert
2018-03-31	[econstr] Forbid calling `to_constr` in open terms.	Emilio Jesus Gallego Arias
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-08-01	Detyping functions are now operating on EConstr.t.	Pierre-Marie Pédrot
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	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias
2017-04-27	Post-rebase warnings (unused opens and 2 unused values)	Gaetan Gilbert
2017-04-24	Porting the firstorder plugin to the new tactic API.	Pierre-Marie Pédrot
2017-02-14	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot
2017-02-14	Hints API using EConstr.	Pierre-Marie Pédrot
2017-02-14	Tacmach API using EConstr.	Pierre-Marie Pédrot
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey
2016-01-20	Update copyright headers.	Maxime Dénès
2015-10-14	Exporting the original unprocessed hint in the hint running function.	Pierre-Marie Pédrot
2015-05-13	Safer typing primitives.	Pierre-Marie Pédrot
2015-05-11	Rationalizing a bit the interface of Hints.	Pierre-Marie Pédrot
2015-04-14	Opaque implementation of auto tactics.	Pierre-Marie Pédrot
2015-01-12	Update headers.	Maxime Dénès
2014-10-07	Splitting out of auto.ml a file hints.ml dedicated to hints so as to	Hugo Herbelin
2014-09-15	Add a "Hint Mode ref (+ \| -)*" hint for setting a global mode	Matthieu Sozeau
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2014-03-01	Fixing pervasive comparisons	Pierre-Marie Pédrot
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-03-23	Minor code cleaning in CArray / CList.	ppedrot
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-09-14	The new ocaml compiler (4.00) has a lot of very cool warnings,	regisgia
2012-08-08	Updating headers.	herbelin