coq - The formal proof system

Age	Commit message (Expand)	Author
2020-07-01	UIP in SProp	Gaëtan Gilbert
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-02-14	Use thunks to univ instead of lazy constr for template typing	Gaëtan Gilbert
2020-02-12	ReferenceVariables error contains a globref instead of a constr	Gaëtan Gilbert
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-11-01	Implement classify on primitive float	Pierre Roux
2019-11-01	Change return type of primitive float comparison	Pierre Roux
2019-11-01	Add primitive float computation in Coq kernel	Guillaume Bertholon
2019-11-01	Declare type of primitives in CPrimitives	Pierre Roux
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-04-12	Remove `constr_of_global_in_context`	Maxime Dénès
2019-03-18	Merge PR #9740: Make NotConvertibleVect exception internal to typeops	Pierre-Marie Pédrot
2019-03-14	Repair relevance marks in-kernel.	Gaëtan Gilbert
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-03-14	Add a non-cumulative impredicative universe SProp.	Gaëtan Gilbert
2019-03-14	Make Sorts.t private	Gaëtan Gilbert
2019-03-11	Make NotConvertibleVect exception internal to typeops	Gaëtan Gilbert
2019-03-11	Nicer error for bad primitive types (through type_errors etc)	Gaëtan Gilbert
2019-02-04	Primitive integers	Maxime Dénès
2018-11-20	Add a check that the return stack of an FProd is indeed empty.	Pierre-Marie Pédrot
2018-11-20	Use a closure for the domain argument of FProd.	Pierre-Marie Pédrot
2018-11-20	More efficient implementation of type_of_apply.	Pierre-Marie Pédrot
2018-10-30	Check univ instances in Typing.	Gaëtan Gilbert
2018-10-26	Merge PR #8684: Remove a few circumvolutions around parameters of inductive e...	Gaëtan Gilbert
2018-10-26	Remove a few circumvolutions around parameters of inductive entries	Maxime Dénès
2018-10-19	Moving Global.constr_of_global_in_context to Typeops.	Hugo Herbelin
2018-10-19	Moving Global.type_of_global_in_context to Typeops.	Hugo Herbelin
2018-10-16	{Univops -> Vars}.universes_of_constr	Gaëtan Gilbert
2018-09-24	[kernel] Compile with almost all warnings enabled.	Emilio Jesus Gallego Arias
2018-07-25	kernel: missing check that all universes are declared.	Matthieu Sozeau
2018-07-24	Projections use index representation	Gaëtan Gilbert
2018-06-26	Remove Sorts.contents	Gaëtan Gilbert
2018-06-23	Change the proj_ind field from MutInd.t to inductive.	Pierre-Marie Pédrot
2018-05-31	Reduce circular dependency constants <-> projections	Gaëtan Gilbert
2018-05-28	Remove vm_conv hook and reorganize kernel files	Maxime Dénès
2018-02-27	Update headers following #6543.	Théo Zimmermann
2017-12-09	[lib] Rename Profile to CProfile	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-09-29	Remove some duplication between Typeops and Nativenorm.	Gaëtan Gilbert
2017-07-26	Removing template polymorphism for definitions.	Pierre-Marie Pédrot
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-16	Clean up universes of constants and inductives	Amin Timany
2017-06-02	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross
2017-04-11	Update various comments to use "template polymorphism"	Gaetan Gilbert
2016-12-12	Replace Typeops by Fast_typeops	Gaetan Gilbert
2016-08-24	CLEANUP: minor readability improvements	Matej Kosik
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-18	Moving the typing_flags to the environment.	Pierre-Marie Pédrot