coq - The formal proof system

Age	Commit message (Expand)	Author
2020-10-21	Deprecate the non-qualified equality functions on kerpairs.	Pierre-Marie Pédrot
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-07-01	UIP in SProp	Gaëtan Gilbert
2020-05-10	No more local reduction functions in Reductionops.	Pierre-Marie Pédrot
2020-03-20	Fix the computation of recursive principles with let-bindings.	Pierre-Marie Pédrot
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-10-24	Raise an anomaly when looking up unknown constant/inductive	Gaëtan Gilbert
2019-07-08	[api] Deprecate GlobRef constructors.	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-05-27	mind_kelim is the highest allowed sort instead of a list	Gaëtan Gilbert
2019-04-10	Remove calls to global env from indrec	Maxime Dénès
2019-04-10	Fix constant order in heads.ml	Maxime Dénès
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-03-14	Add a non-cumulative impredicative universe SProp.	Gaëtan Gilbert
2018-11-06	Move debug term printer to kernel	Maxime Dénès
2018-10-18	[api] Qualify access to `Nametab`	Emilio Jesus Gallego Arias
2018-10-07	[api] Deprecate `evar_map` ref combinators.	Emilio Jesus Gallego Arias
2018-10-05	[kernel] Remove section paths from `KerName.t`	Maxime Dénès
2018-09-28	Functionalizing calls to the environment in Himsg.	Hugo Herbelin
2018-07-24	Projections use index representation	Gaëtan Gilbert
2018-07-03	Remove unused env argument to fresh_sort_in_family	Gaëtan Gilbert
2018-06-13	[vernac] Add option to force building really mutual induction schemes	Matthieu Sozeau
2018-05-25	Remove some occurrences of Evd.empty	Maxime Dénès
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-13	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias
2017-11-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
2017-11-06	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-06	Remove the Sigma (monotonous state) API.	Maxime Dénès
2017-06-02	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross
2017-02-14	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot
2017-02-14	Introducing contexts parameterized by the inner term type.	Pierre-Marie Pédrot
2017-02-14	Reductionops now return EConstrs.	Pierre-Marie Pédrot
2017-02-14	Cases API using EConstr.	Pierre-Marie Pédrot
2017-02-14	Reductionops 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-06	Disallow dependent case on prim records w/o eta	Matthieu Sozeau
2016-07-06	Renaming to more generic has_dependent_elim test	Matthieu Sozeau
2016-07-06	Move is_prim... to Inductiveops and correct Scheme	Matthieu Sozeau
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-06-29	A new infrastructure for warnings.	Maxime Dénès
2016-05-31	Feedback cleanup	Emilio Jesus Gallego Arias
2016-05-04	Merge branch 'v8.5'	Pierre-Marie Pédrot
2016-05-03	Use the canonical name when looking for an eliminator (bug #4670).	Guillaume Melquiond
2016-02-09	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik
2016-01-29	Merge branch 'v8.5'	Pierre-Marie Pédrot