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-03-04	Rename Ephemeron -> CEphemeron.	Maxime Dénès
2015-10-28	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi
2015-10-02	Univs: fix evar_map leaks bugs in Function	Matthieu Sozeau
2015-04-23	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond
2015-04-14	Function now supports puniveres	jforest
2014-06-08	Moving hook code from Future to Lemmas. This seemed to disrupt compilation of	Pierre-Marie Pédrot
2014-06-08	Enforce a correct exception handling in declaration_hooks	Enrico Tassi
2014-05-06	Fix funind w.r.t. universes	Matthieu Sozeau
2014-05-06	Correct rebase on STM code. Thanks to E. Tassi for help on dealing with	Matthieu Sozeau
2014-05-06	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau
2013-12-04	Factoring(continued).	Arnaud Spiwack
2013-12-04	Refactoring: storing more information in the terminator closure.	Arnaud Spiwack
2013-12-04	The commands that initiate proofs are now in charge of what happens when proo...	Arnaud Spiwack
2013-11-25	Remove the Hiddentac module.	Arnaud Spiwack
2013-11-02	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack
2013-10-18	declaration_hooks use Ephemeron	gareuselesinge
2013-08-22	Less "Coq" strings everywhere	letouzey
2013-08-08	get rid of closures in global/proof state	gareuselesinge
2013-05-09	Use definition_entry to declare local definitions	gareuselesinge
2013-04-22	code simplifications concerning Summary	letouzey
2013-04-02	Revised infrastructure for lazy loading of opaque proofs	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 15)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 9)	letouzey
2013-03-13	Restrict (try...with...) to avoid catching critical exn (part 7)	letouzey
2013-03-12	invalid_arg instead of raise (Invalid_argement ...)	letouzey
2013-03-11	Added a Local Definition vernacular command. This type of definition	ppedrot
2013-02-26	kernel/declarations becomes a pure mli	letouzey
2013-02-19	Dir_path --> DirPath	letouzey
2013-02-18	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey
2013-01-28	Uniformization of the "anomaly" command.	ppedrot
2012-12-18	Modulification of Label	ppedrot
2012-12-14	Modulification of dir_path	ppedrot
2012-12-14	Modulification of identifier	ppedrot
2012-10-02	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey
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-29	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey
2012-05-29	Decl_kinds becomes a pure mli file, remaining ops in new file kindops.ml	letouzey
2012-03-02	Noise for nothing	pboutill
2012-03-01	New version of recdef :	jforest
2011-12-12	Proof using ...	gareuselesinge
2011-11-24	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot
2011-11-02	Add type annotations around all calls to Libobject.declare_object	letouzey
2011-04-13	Revert "Add [Polymorphic] flag for defs"	msozeau
2011-04-13	Add [Polymorphic] flag for defs	msozeau
2011-04-03	Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacks	letouzey
2010-12-23	Rename rawterm.ml into glob_term.ml	glondu
2010-12-23	Change of nomenclature: rawconstr -> glob_constr	glondu