coq - The formal proof system

Age	Commit message (Expand)	Author
2020-06-25	Generate names for anonymous polymorphic universes	Gaëtan Gilbert
2020-06-25	Make compute_instance_binders internal to UState	Gaëtan Gilbert
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2018-12-12	Merge PR #9150: [doc] Enable Warning 50 [incorrect doc comment] and fix comme...	Maxime Dénès
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-12-06	Revise API for global universes.	Gaëtan Gilbert
2018-12-06	Fix race condition triggered by fresh universe generation	Maxime Dénès
2018-11-16	Print universe names in subtyping error instead of Var(x).	Gaëtan Gilbert
2018-11-09	Use arrays of names instead of lists in abstract universe names.	Pierre-Marie Pédrot
2018-11-09	Remove remnants of polymorphic instance name registration.	Pierre-Marie Pédrot
2018-11-09	Actually store the bound name information in the abstract universe context.	Pierre-Marie Pédrot
2018-11-09	Adding universe names to polymorphic entry instances.	Pierre-Marie Pédrot
2018-10-16	Deprecate Global.universes_of_global (replaced by environ version)	Gaëtan Gilbert
2018-10-05	[kernel] Remove section paths from `KerName.t`	Maxime Dénès
2018-09-27	Fix #8478: Undeclared universe anomaly with sections	Gaëtan Gilbert
2018-09-21	Universe binders are Id, not Name. Never print Var.	Gaëtan Gilbert
2018-09-21	Best-effort hack to provide a meaningful name for anonymous bound universes.	Pierre-Marie Pédrot
2018-09-21	Store universe binder names as a mere list of names.	Pierre-Marie Pédrot
2018-09-21	Removing calls to AUContext.instance.	Pierre-Marie Pédrot
2018-09-12	Move maps & sets indexed by GlobRef.t into the kernel	Vincent Laporte
2018-06-18	Remove reference name type.	Maxime Dénès
2018-06-12	[api] Misctypes removal: miscellaneous aliases.	Emilio Jesus Gallego Arias
2018-05-17	Split off Universes functions dealing with names.	Gaëtan Gilbert