coq - The formal proof system

Age	Commit message (Expand)	Author
2020-02-13	Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)	Gaëtan Gilbert
2020-02-13	Delete unused comment	Gaëtan Gilbert
2020-02-13	Don't duplicate the inductive keyword for each block elt when parsing	Gaëtan Gilbert
2020-02-13	Merge PR #11407: [mltop] Store digest of modules used to compile files.	Gaëtan Gilbert
2020-02-13	Merge PR #11521: Remove Goptions.opt_name field	Pierre-Marie Pédrot
2020-02-13	Merge PR #11424: Check instance length in type_of_{inductive,constructor}	Pierre-Marie Pédrot
2020-02-12	Remove Goptions.opt_name field	Gaëtan Gilbert
2020-02-12	Check instance length in type_of_{inductive,constructor}	Gaëtan Gilbert
2020-02-12	ReferenceVariables error contains a globref instead of a constr	Gaëtan Gilbert
2020-02-12	Merge PR #11546: Remove the Template Check option.	Gaëtan Gilbert
2020-02-11	Fixing some residual bugs of PR #10202 (manual implicit args in subterms).	Hugo Herbelin
2020-02-11	Merge PR #11235: Add syntax for non maximal implicit arguments	Hugo Herbelin
2020-02-09	Remove the Template Check option.	Pierre-Marie Pédrot
2020-02-06	unsafe_type_of -> type_of in ComCoercion.build_id_coercion	Gaëtan Gilbert
2020-02-06	unsafe_type_of -> get_type_of in Auto_ind_decl.do_replace_bl	Gaëtan Gilbert
2020-02-06	unsafe_type_of -> get_type_of in ComProgramFixpoint.build_wellfounded	Gaëtan Gilbert
2020-02-06	Merge PR #11478: Nicer kernel universe error for inductives	Pierre-Marie Pédrot
2020-02-06	Merge PR #10835: Accepting a few more variants of format for recursive notati...	Pierre-Marie Pédrot
2020-02-04	Add syntax for non maximally inserted implicit arguments	SimonBoulier
2020-01-31	More tolerant in format for recursive notations.	Hugo Herbelin
2020-01-30	[exn] Don't reraise in exception printers	Emilio Jesus Gallego Arias
2020-01-30	Notations: Fixing a wrong location in format.	Hugo Herbelin
2020-01-30	Merge PR #11307: Remove the hacks relying on hardwired libobject tags.	Maxime Dénès
2020-01-29	[rfc] [mltop] Removal of dynamic loading of object and `.ml` files	Emilio Jesus Gallego Arias
2020-01-29	Nicer kernel universe error for inductives	Gaëtan Gilbert
2020-01-29	Merge PR #11408: [mltop] Remove error handling hacks in favor of default meth...	Pierre-Marie Pédrot
2020-01-28	Remove dead code in Globnames.	Pierre-Marie Pédrot
2020-01-28	Merge PR #11379: [ocaml] Remove Custom Backtrace module in favor of OCaml's	Pierre-Marie Pédrot
2020-01-27	cleanup: Lib.freeze doesn't use its [~marshallable] argument	Gaëtan Gilbert
2020-01-25	Merge PR #11025: Add Set NativeCompute Timing	Maxime Dénès
2020-01-21	Typo in an anomaly message.	Hugo Herbelin
2020-01-16	[mltop] Remove error handling hacks in favor of default methods.	Emilio Jesus Gallego Arias
2020-01-16	[mltop] Store digest of modules used to compile files.	Emilio Jesus Gallego Arias
2020-01-15	[ocaml] Remove Custom Backtrace module in favor of OCaml's	Emilio Jesus Gallego Arias
2020-01-13	Merge PR #11280: Fix #11195 and add other improvements: try loading .vio (and...	Pierre-Marie Pédrot
2020-01-09	Fix build after merge of #11164	Gaëtan Gilbert
2020-01-09	Merge PR #11164: [CS] allow Let variable to be canonical	Pierre-Marie Pédrot
2020-01-08	Add Set NativeCompute Timing	Jason Gross
2019-12-31	Merge PR #11338: Remove uses of Global in Evd API.	Gaëtan Gilbert
2019-12-29	Merge PR #11334: Fixes a small bug exposing an _ANONYMOUS_REL in a unificatio...	Pierre-Marie Pédrot
2019-12-28	Extend `Print Canonical Projections` with a search functionality	Kazuhiko Sakaguchi
2019-12-27	Merge PR #11315: Ensure that a custom entry cannot be defined twice.	Hugo Herbelin
2019-12-26	Remove uses of Global in Evd API.	Pierre-Marie Pédrot
2019-12-24	[Attributes] accept #[canonical] (Let\|Definition)	Enrico Tassi
2019-12-24	[CS] Allow a variable introduced with Let to be a canonical instance	Enrico Tassi
2019-12-23	Merge PR #11293: Rename files with Class in their name to make their role cle...	Hugo Herbelin
2019-12-23	Fixes a small bug exposing an _ANONYMOUS_REL in a unification error message.	Hugo Herbelin
2019-12-23	Merge PR #11274: [library] [cleanup] Remove code duplication.	Pierre-Marie Pédrot
2019-12-22	Rename files with Class in their name to make their role clearer.	Pierre-Marie Pédrot
2019-12-22	Ensure that a custom entry cannot be defined twice.	Pierre-Marie Pédrot