coq - The formal proof system

Age	Commit message (Expand)	Author
2017-11-22	[api] Deprecate Term destructors, move to Constr	Emilio Jesus Gallego Arias
2017-11-21	Merge PR #6185: [parser] Remove unnecessary statically initialized hook.	Maxime Dénès
2017-11-20	Merge PR #6125: Fixing remaining problems with bug #5762 and PR #1120 (clause...	Maxime Dénès
2017-11-19	[parser] Remove unnecessary statically initialized hook.	Emilio Jesus Gallego Arias
2017-11-13	[api] Another large deprecation, `Nameops`	Emilio Jesus Gallego Arias
2017-11-08	Fixing a remaining "coqdoc" problem with bug #5762 and pr #1120.	Hugo Herbelin
2017-11-06	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias
2017-10-20	Merge PR #1120: Fixing BZ#5762 (supporting implicit arguments in "where" clau...	Maxime Dénès
2017-10-17	[stm] Remove state-handling from Futures.	Emilio Jesus Gallego Arias
2017-10-05	Fixing #5765 (an anomaly with 'pat in parameters of inductive definition).	Hugo Herbelin
2017-10-05	Fixing #5762 (supporting imp. args. in "where" clause of an inductive def.).	Hugo Herbelin
2017-09-26	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès
2017-09-20	[flags] Flag `open Flags`	Emilio Jesus Gallego Arias
2017-09-19	Don't lose names in UState.universe_context.	Gaëtan Gilbert
2017-09-19	Allow declaring universe constraints at definition level.	Matthieu Sozeau
2017-09-04	Making detyping potentially lazy.	Pierre-Marie Pédrot
2017-08-31	Merge PR #980: Adding combinators + a canonical renaming in List, Option, Name	Maxime Dénès
2017-08-29	Adapting code to renaming fold_map/fold_map' into fold_left_map/fold_right_map	Hugo Herbelin
2017-08-01	Remove understand_tcc_evars.	Maxime Dénès
2017-07-04	Merge branch 'v8.6'	Pierre-Marie Pédrot
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-20	[vernac] Remove forward hooks from Obligations.	Emilio Jesus Gallego Arias
2017-06-20	[vernac] Remove unused hooks.	Emilio Jesus Gallego Arias
2017-06-16	Clean up universes of constants and inductives	Amin Timany
2017-06-16	Fix bugs and add an option for cumulativity	Amin Timany
2017-06-16	Fix bugs	Amin Timany
2017-06-16	Squashed commit of the following:	Amin Timany
2017-06-16	Change the place of inference after sect discharge	Amin Timany
2017-06-16	Subtyping inference for inductoves and records	Amin Timany
2017-06-16	Add subtyping inference for inductive types	Amin Timany
2017-06-16	Using UInfoInd for universes in inductive types	Amin Timany
2017-06-16	Extend definition of inductives to include subtyping info	Amin Timany
2017-06-11	[proof] Deprecate redundant wrappers.	Emilio Jesus Gallego Arias
2017-06-06	Remove the Sigma (monotonous state) API.	Maxime Dénès
2017-06-06	Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...	Maxime Dénès
2017-06-02	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross
2017-06-01	Merge PR#696: Trunk+cleanup constr of global	Maxime Dénès
2017-06-01	Merge PR#561: Improving the Name API	Maxime Dénès
2017-05-31	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin
2017-05-31	More precise on preventing clash between bound vars name and hidden impargs.	Hugo Herbelin
2017-05-31	Fixing a failure to interpret some local implicit arguments in Inductive.	Hugo Herbelin
2017-05-30	Support for using type information to infer more precise evar sources.	Hugo Herbelin
2017-05-29	Command.ml cleanup: remove constr_of_global calls	Matthieu Sozeau
2017-05-29	Merge PR#512: [cleanup] Unify all calls to the error function.	Maxime Dénès
2017-05-27	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias
2017-05-27	[coqlib] Deprecate redundant Coqlib functions.	Emilio Jesus Gallego Arias
2017-05-24	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias
2017-05-02	Merge PR#582: Fix warnings	Maxime Dénès
2017-04-28	Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...	Maxime Dénès
2017-04-27	Fix omitted labels in function calls	Gaetan Gilbert