coq - The formal proof system

Age	Commit message (Expand)	Author
2020-08-22	Namegen.visible_ids: fixing what seems to be typos.	Hugo Herbelin
2020-07-06	Primitive persistent arrays	Maxime Dénès
2020-07-01	UIP in SProp	Gaëtan Gilbert
2020-04-06	Clean and fix definitions of options.	Théo Zimmermann
2020-03-18	Update headers in the whole code base.	Théo Zimmermann
2020-02-29	Be robust in calculating visible ids for non-registered constants.	Pierre-Marie Pédrot
2020-02-12	Remove Goptions.opt_name field	Gaëtan Gilbert
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-07-08	[api] Deprecate GlobRef constructors.	Emilio Jesus Gallego Arias
2019-06-17	Update ml-style headers to new year.	Théo Zimmermann
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-02-18	[Namegen] Use Global.exists_objlabel in `next_global_ident_away`	Vincent Laporte
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-11-28	[options] New helper for creation of boolean options plus reference.	Emilio Jesus Gallego Arias
2018-11-23	s/let _ =/let () =/ in some places (mostly goptions related)	Gaëtan Gilbert
2018-10-18	[api] Qualify access to `Nametab`	Emilio Jesus Gallego Arias
2018-10-05	[kernel] Remove section paths from `KerName.t`	Maxime Dénès
2018-09-12	Move maps & sets indexed by GlobRef.t into the kernel	Vincent Laporte
2018-06-26	Remove Sorts.contents	Gaëtan Gilbert
2018-06-12	[api] Misctypes removal: several moves:	Emilio Jesus Gallego Arias
2018-05-30	[api] Remove deprecated object from `Term`	Emilio Jesus Gallego Arias
2018-03-08	Merge PR #6899: [compat] Remove "Standard Proposition Elimination"	Maxime Dénès
2018-03-08	Merge PR #6582: Mangle auto-generated names	Maxime Dénès
2018-03-03	[compat] Remove "Standard Proposition Elimination"	Emilio Jesus Gallego Arias
2018-02-27	Update headers following #6543.	Théo Zimmermann
2018-02-17	Implement name mangling option	Jasper Hugunin
2017-11-06	[api] Deprecate all legacy uses of Names in core.	Emilio Jesus Gallego Arias
2017-11-05	Fixing a cause of failure of evar_map printer in debugger.	Hugo Herbelin
2017-10-28	Fixing #5401 (printing of patterns with bound anonymous variables).	Hugo Herbelin
2017-10-06	Merge PR #1119: Fixing bug BZ#5769 (generating a name "_" out of a type "_som...	Maxime Dénès
2017-10-05	Fixing BZ#5769 (variable of type "_something" was named after invalid "_").	Hugo Herbelin
2017-09-28	Efficient computation of the names contained in an environment.	Pierre-Marie Pédrot
2017-09-28	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot
2017-07-04	Bump year in headers.	Pierre-Marie Pédrot
2017-06-14	Deprecate options that were introduced for compatibility with 8.4.	Guillaume Melquiond
2017-06-14	Remove support for Coq 8.4.	Guillaume Melquiond
2017-05-24	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias
2017-04-01	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot
2017-02-14	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot
2016-10-30	Reordering Termops w.r.t. Evd and Namegen in engine folder.	Pierre-Marie Pédrot
2016-10-20	CLEANUP: Namegen.to_avoid	Matej Kosik
2016-10-19	CLEANUP: rename "Nameops.lift_subscript" to "Nameops.increment_subscript".	Matej Kosik
2016-08-24	CLEANUP: minor readability improvements	Matej Kosik
2016-08-17	Merge branch 'v8.6'	Pierre-Marie Pédrot
2016-08-17	Fixing printing in debugger (no global env in debugger).	Hugo Herbelin
2016-08-11	CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function	Matej Kosik
2016-08-11	CLEANUP: removing a call of "Context.Rel.Declaration.to_tuple" function	Matej Kosik