coq - The formal proof system

Age	Commit message (Expand)	Author
2020-10-21	Introduce an Ind module in the Names API.	Pierre-Marie Pédrot
2020-10-21	Deprecate the non-qualified equality functions on kerpairs.	Pierre-Marie Pédrot
2020-08-20	Use properly fresh names for Scheme Equality	Jasper Hugunin
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-07-01	UIP in SProp	Gaëtan Gilbert
2020-05-19	[universes] [api] Provide UState.from_env	Emilio Jesus Gallego Arias
2020-05-10	No more local reduction functions in Reductionops.	Pierre-Marie Pédrot
2020-05-03	[funind] Remove use of low-level entries in scheme generation.	Emilio Jesus Gallego Arias
2020-04-29	Merge the call to tclEFFECTS into find_scheme.	Pierre-Marie Pédrot
2020-04-29	Remove dead user-facing code in scheme generation.	Pierre-Marie Pédrot
2020-04-28	Add comment about decide equality dependence computation.	Pierre-Marie Pédrot
2020-04-28	Return an option in lookup_scheme.	Pierre-Marie Pédrot
2020-04-28	Stop relying on side-effects for recursive scheme declaration.	Pierre-Marie Pédrot
2020-04-15	[proof] Merge `Proof_global` into `Declare`	Emilio Jesus Gallego Arias
2020-04-15	[proof] Move proof_global functionality to Proof_global from Pfedit	Emilio Jesus Gallego Arias
2020-03-28	Fix #11941: anomaly in equality schemes	Gaëtan Gilbert
2020-03-19	[declare] Remove one use of inline_private_constants	Emilio Jesus Gallego Arias
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-06	unsafe_type_of -> get_type_of in Auto_ind_decl.do_replace_bl	Gaëtan Gilbert
2019-12-10	Simplify internal flags in scheme declarations.	Pierre-Marie Pédrot
2019-11-21	[coq] Untabify the whole ML codebase.	Emilio Jesus Gallego Arias
2019-11-01	Add primitive float computation in Coq kernel	Guillaume Bertholon
2019-08-26	Make kernel parametric on the lowest universe and fix #9294	Matthieu Sozeau
2019-07-08	[api] Deprecate GlobRef constructors.	Emilio Jesus Gallego Arias
2019-06-25	Move the internal_flag type from Declare to Ind_tables.	Pierre-Marie Pédrot
2019-06-24	[proof] Remove last case of optional `?poly` arguments.	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
2019-06-11	Remove the side-effect role from the kernel.	Pierre-Marie Pédrot
2019-05-27	mind_kelim is the highest allowed sort instead of a list	Gaëtan Gilbert
2019-03-14	Add relevance marks on binders.	Gaëtan Gilbert
2019-02-04	Primitive integers	Maxime Dénès
2018-12-09	[doc] Enable Warning 50 [incorrect doc comment] and fix comments.	Emilio Jesus Gallego Arias
2018-10-19	Deprecating Global.type_of_global_in_context.	Hugo Herbelin
2018-10-18	[universes] deprecate constr_of_global	Matthieu Sozeau
2018-10-10	[coqlib] Rebindable Coqlib namespace.	Emilio Jesus Gallego Arias
2018-09-27	Using Constant.change_label (better level of abstraction to build kernel names).	Hugo Herbelin
2018-09-27	Scheme Equality: support for working in a context of Parameters.	Hugo Herbelin
2018-09-27	Fixing a Scheme Equality anomaly with constants bound to inductive.	Hugo Herbelin
2018-09-27	Fixing a typo in a comment.	Hugo Herbelin
2018-09-27	Fixing #4859 (anomaly with Scheme called on inductive type with indices).	Hugo Herbelin
2018-09-27	Fixing #4612 (anomaly with Scheme called on unsupported inductive type).	Hugo Herbelin
2018-09-23	Checking if low-level name printers are used on purpose or not.	Hugo Herbelin
2018-08-22	Fix #8251: remove "the the" occurrences	Gaëtan Gilbert
2018-06-12	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias
2018-06-04	[vernac] Switch back `auto_ind_decl` to Constr.	Emilio Jesus Gallego Arias
2018-05-29	Fix #6951: Unexpected error during scheme creation.	Pierre-Marie Pédrot
2018-05-23	Collecting Array.smart_* functions into a module Array.Smart.	Hugo Herbelin
2018-05-17	Split off Universes functions dealing with generating new universes.	Gaëtan Gilbert
2018-05-04	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias