coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Tracking careless uses of slow name lookup.	Pierre-Marie Pédrot	2016-09-09
*	errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...	Pierre Letouzey	2016-07-03
*	Separate flags for fix/cofix/match reduction and clean reduction function names.	Maxime Dénès	2016-07-01
*	CLEANUP: Context.{Rel,Named}.Declaration.t	Matej Kosik	2016-02-09
*	Merge branch 'v8.5'	Pierre-Marie Pédrot	2016-01-21
\|\
\| *	Update copyright headers.	Maxime Dénès	2016-01-20
* \|	CLEANUP: kernel/context.ml{,i}	Matej Kosik	2016-01-11
* \|	Merge branch 'v8.5'	Pierre-Marie Pédrot	2015-10-29
\|\\|
\| *	Univs: local names handling.	Matthieu Sozeau	2015-10-28
* \|	Boxing the Goal.enter primitive into a record type.	Pierre-Marie Pédrot	2015-10-20
\|/
*	Fix some typos.	Guillaume Melquiond	2015-10-13
*	Univs: Add universe binding lists to definitions	Matthieu Sozeau	2015-09-14
*	Fix bug #2775: Correct handling of universes in leminv.	Matthieu Sozeau	2015-02-12
*	Update headers.	Maxime Dénès	2015-01-12
*	Switch the few remaining iso-latin-1 files to utf8	Pierre Letouzey	2014-12-09
*	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-12
*	Renaming goal-entering functions.	Pierre-Marie Pédrot	2014-09-06
*	Clenvtac.res_pf is in the new tactic monad.	Pierre-Marie Pédrot	2014-06-24
*	Proofs now take and return an evar_universe_context, simplifying interfaces	Matthieu Sozeau	2014-06-18
*	- Fix bug preventing apply from unfolding Fixpoints.	Matthieu Sozeau	2014-05-06
*	Rework handling of universes on top of the STM, allowing for delayed	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Removing dead code, thanks to new OCaml warnings and a bit of scripting.	Pierre-Marie Pédrot	2014-04-23
*	Removing the compatibility layer from Leminv. Also removed an undocumented	Pierre-Marie Pédrot	2014-04-22
*	Define Tactics.bring_hyps in the new monad.	Pierre-Marie Pédrot	2014-03-28
*	Remove many superfluous 'open' indicated by ocamlc -w +33	Pierre Letouzey	2014-03-05
*	Qed: feedback when type checking is done	Enrico Tassi	2013-12-24
*	Allowing proofs starting with a non-empty evarmap.	ppedrot	2013-11-04
*	Tachmach.New is now in Proofview.Goal.enter style.	aspiwack	2013-11-02
*	More Proofview.Goal.enter.	aspiwack	2013-11-02
*	The tactic [admit] exits with the "unsafe" status.	aspiwack	2013-11-02
*	Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.	aspiwack	2013-11-02
*	Getting rid of Goal.here, and all the related exceptions and combinators.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	More monomorphic List.mem + List.assoc + ...	letouzey	2013-10-24
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Splitting Term into five unrelated interfaces:	ppedrot	2013-04-29
*	Added a Local Definition vernacular command. This type of definition	ppedrot	2013-03-11
*	New implementation of the conversion test, using normalization by evaluation to	mdenes	2013-01-22
*	Modulification of identifier	ppedrot	2012-12-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-09-14
*	Updating headers.	herbelin	2012-08-08
*	Noise for nothing	pboutill	2012-03-02
*	Proof using ...	gareuselesinge	2011-12-12
*	Moved allow_K to a unification flag	herbelin	2011-06-10
*	Revert "Add [Polymorphic] flag for defs"	msozeau	2011-04-13