coq - The formal proof system

Age	Commit message (Expand)	Author
2016-07-03	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey
2016-06-18	Reuse the typing_flags datatype for inductives.	Pierre-Marie Pédrot
2016-06-16	Merge PR #79: Let the kernel assume that a (co-)inductive type is positive.	Pierre-Marie Pédrot
2016-06-15	Remove the syntax changes introduced by this branch.	Pierre-Marie Pédrot
2016-06-02	A slight phase of documentation and uniformization of names of	Hugo Herbelin
2016-05-31	Feedback cleanup	Emilio Jesus Gallego Arias
2016-02-09	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik
2016-01-11	CLEANUP: kernel/context.ml{,i}	Matej Kosik
2015-11-18	Fix a bug preventing the generation of graphs when doing multiple	Matthieu Sozeau
2015-10-02	Univs: fix after rebase (from_ctx/from_env)	Matthieu Sozeau
2015-10-02	Univs: fix evar_map leaks bugs in Function	Matthieu Sozeau
2015-09-14	Univs: Add universe binding lists to definitions	Matthieu Sozeau
2015-06-24	Add corresponding field in `VernacInductive`.	Arnaud Spiwack
2015-05-13	Safer typing primitives.	Pierre-Marie Pédrot
2015-04-14	Function now supports puniveres	jforest
2015-02-23	Fix some typos in comments.	Guillaume Melquiond
2014-12-11	handling Functional Scheme for required but not imported modules	Julien Forest
2014-12-08	Closing bug 3837	Julien Forest
2014-09-17	Revert specific syntax for primitive projections, avoiding ugly	Matthieu Sozeau
2014-09-12	Uniformisation of the order of arguments env and sigma.	Hugo Herbelin
2014-09-12	Referring to evars by names. Added a parser for evars (but parsing of	Hugo Herbelin
2014-09-08	Parsing of Type@{max(i,j)}.	Matthieu Sozeau
2014-09-04	Remove [Infer] option of records.	Arnaud Spiwack
2014-09-04	Print [Variant] types with the keyword [Variant].	Arnaud Spiwack
2014-08-01	A tentative uniform naming policy in module Inductiveops.	Hugo Herbelin
2014-05-06	Adapt Y. Bertot's path on private inductives (now the keyword is "Private").	Yves Bertot
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-10-24	More monomorphic List.mem + List.assoc + ...	letouzey
2013-10-23	cList: set-as-list functions are now with an explicit comparison	letouzey
2013-09-27	Removing a bunch of generic equalities.	ppedrot
2013-05-09	A uniformization step around understand_* and interp_* functions.	herbelin
2013-04-29	Merging Context and Sign.	ppedrot
2013-04-29	Splitting Term into five unrelated interfaces:	ppedrot
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-12-18	Modulification of name	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-10-31	correcting a little bug in Function	jforest
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
2012-09-15	Some documentation and cleaning of CList and Util interfaces.	ppedrot
2012-09-14	As r15801: putting everything from Util.array_* to CArray.*.	ppedrot
2012-09-14	Moving Utils.list_* to a proper CList module, which includes stdlib	ppedrot
2012-09-14	This patch removes unused "open" (automatically generated from	regisgia
2012-06-22	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot
2012-06-01	Getting rid of Pp.msgnl and Pp.message.	ppedrot
2012-05-30	Getting rid of Pp.msg	ppedrot
2012-05-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	Basic stuff about constr_expr migrated from topconstr to constrexpr_ops	letouzey
2012-05-29	Stuff about notation_constr (ex-aconstr) now in notation_ops.ml	letouzey
2012-05-29	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey