coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Making Proof_global terminator generic in external tactics.	Pierre-Marie Pédrot	2016-09-08
*	Rework treatment of default transparency of obligations	Matthieu Sozeau	2016-06-27
*	Moving the use of Tactic_option from Obligations to G_obligations.	Pierre-Marie Pédrot	2016-03-19
*	Implement support for universe binder lists in Instance and Program Fixpoint/...	Matthieu Sozeau	2016-01-23
*	Update copyright headers.	Maxime Dénès	2016-01-20
*	Allow program hooks to see the refined universe_context at the end of a	Matthieu Sozeau	2015-11-19
*	Avoid type checking private_constants (side_eff) again during Qed (#4357).	Enrico Tassi	2015-10-28
*	Removing dead code.	Pierre-Marie Pédrot	2015-02-02
*	Add the possibility of defining opaque terms with program.	mlasson	2015-01-21
*	Update headers.	Maxime Dénès	2015-01-12
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18
*	Moving hook code from Future to Lemmas. This seemed to disrupt compilation of	Pierre-Marie Pédrot	2014-06-08
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Removing useless meta-related functions.	Pierre-Marie Pédrot	2013-12-03
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	At least made the evar type opaque! There are still 5 remaining unsafe	ppedrot	2013-09-18
*	get rid of closures in global/proof state	gareuselesinge	2013-08-08
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Allowing (Co)Fixpoint to be defined local and Let-style.	ppedrot	2013-03-11
*	Modulification of identifier	ppedrot	2012-12-14
*	Moved Intset and Intmap to Int namespace.	ppedrot	2012-12-14
*	Updating headers.	herbelin	2012-08-08
*	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
*	New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr	letouzey	2012-05-29
*	Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd	letouzey	2012-05-29
*	Fix bugs related to Program integration.	msozeau	2012-03-19
*	Fix merge and add missing file.	msozeau	2012-03-14
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14