coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Funind API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Equality API using EConstr.	Pierre-Marie Pédrot	2017-02-14
*	Revert "Merge remote-tracking branch 'github/pr/283' into trunk"	Maxime Dénès	2016-09-22
*	Stylistic improvements in intf/decl_kinds.mli.	Maxime Dénès	2016-09-20
*	Make the user_err header an optional parameter.	Emilio Jesus Gallego Arias	2016-08-19
*	Remove errorlabstrm in favor of user_err	Emilio Jesus Gallego Arias	2016-08-19
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Rename Ephemeron -> CEphemeron.	Maxime Dénès	2016-03-04
*	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
*	Univs: fix evar_map leaks bugs in Function	Matthieu Sozeau	2015-10-02
*	Remove almost all the uses of string concatenation when building error messages.	Guillaume Melquiond	2015-04-23
*	Function now supports puniveres	jforest	2015-04-14
*	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-06-08
*	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	2014-05-06
*	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-12-04
*	Remove the Hiddentac module.	Arnaud Spiwack	2013-11-25
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	declaration_hooks use Ephemeron	gareuselesinge	2013-10-18
*	Less "Coq" strings everywhere	letouzey	2013-08-22
*	get rid of closures in global/proof state	gareuselesinge	2013-08-08
*	Use definition_entry to declare local definitions	gareuselesinge	2013-05-09
*	code simplifications concerning Summary	letouzey	2013-04-22
*	Revised infrastructure for lazy loading of opaque proofs	letouzey	2013-04-02
*	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-13
*	invalid_arg instead of raise (Invalid_argement ...)	letouzey	2013-03-12
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11
*	kernel/declarations becomes a pure mli	letouzey	2013-02-26
*	Dir_path --> DirPath	letouzey	2013-02-19
*	Minor code cleanups, especially take advantage of Dir_path.is_empty	letouzey	2013-02-18
*	Uniformization of the "anomaly" command.	ppedrot	2013-01-28
*	Modulification of Label	ppedrot	2012-12-18
*	Modulification of dir_path	ppedrot	2012-12-14
*	Modulification of identifier	ppedrot	2012-12-14
*	Remove some more "open" and dead code thanks to OCaml4 warnings	letouzey	2012-10-02
*	This patch removes unused "open" (automatically generated from	regisgia	2012-09-14
*	Added an indirection with respect to Loc in Compat. As many [open Compat]	ppedrot	2012-06-22
*	Getting rid of Pp.msgnl and Pp.message.	ppedrot	2012-06-01
*	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-05-29
*	Noise for nothing	pboutill	2012-03-02
*	New version of recdef :	jforest	2012-03-01
*	Proof using ...	gareuselesinge	2011-12-12
*	Added a DEPRECATED flag in declaration of options. For now only two options a...	ppedrot	2011-11-24