coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	[emacs] [toplevel] Make emacs flag local to the toplevel.	Emilio Jesus Gallego Arias	2017-06-01
*	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
*	Removing the tclWEAK_PROGRESS tactical.	Pierre-Marie Pédrot	2017-04-24
*	Removing the tclNOTSAMEGOAL primitive from the API.	Pierre-Marie Pédrot	2017-04-24
*	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
*	Merge PR #244.	Pierre-Marie Pédrot	2016-09-08
\|\
* \	Merge remote-tracking branch 'v8.6' into trunk	Matej Kosik	2016-08-25
\|\ \
* \| \|	CLEANUP: minor readability improvements	Matej Kosik	2016-08-24
\| \| *	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
\| \|/ \|/\|
\| *	[pp] Fix newline issues.	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
*	Feedback cleanup	Emilio Jesus Gallego Arias	2016-05-31
*	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
\|/
*	Fixed (and changed) infoH.	Pierre Courtieu	2015-10-21
*	Update headers.	Maxime Dénès	2015-01-12
*	msg_info now puts infomsg tag in emacs mode.	Pierre Courtieu	2014-12-16
*	Getting rid of Exninfo hacks.	Pierre-Marie Pédrot	2014-12-16
*	Improving error message when applying rewrite to an expression which is not a...	Hugo Herbelin	2014-08-18
*	More self-contained code for tclWITHHOLES.	Pierre-Marie Pédrot	2014-08-15
*	Removing unused Refiner.tclWITHHOLES.	Pierre-Marie Pédrot	2014-08-15
*	Improving tclWITHHOLES which did not see undefined evars up to	Hugo Herbelin	2014-06-13
*	Cleanup in Univ, moving code for UniverseConstraints outside the kernel in Un...	Matthieu Sozeau	2014-06-10
*	Adding a new Control file centralizing the control options of Coq.	Pierre-Marie Pédrot	2014-06-07
*	- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...	Matthieu Sozeau	2014-05-08
*	- Fix comparison of universes.	Matthieu Sozeau	2014-05-06
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Removing unused functions in Refiner.	Pierre-Marie Pédrot	2014-04-06
*	Removing the Change_evar refiner rule.	Pierre-Marie Pédrot	2014-03-31
*	Remove some dead-code (thanks to ocaml warnings)	Pierre Letouzey	2014-03-05
*	Cleanup of comments.	aspiwack	2013-11-02
*	Makes the new Proofview.tactic the basic type of Ltac.	aspiwack	2013-11-02
*	cList: set-as-list functions are now with an explicit comparison	letouzey	2013-10-23
*	Moving side effects into evar_map. There was no reason to keep another	ppedrot	2013-10-05
*	State Transaction Machine	gareuselesinge	2013-08-08
*	Getting rid of LtacLocated exception transformer.	ppedrot	2013-05-28
*	Merging Context and Sign.	ppedrot	2013-04-29
*	Restrict (try...with...) to avoid catching critical exn (part 12)	letouzey	2013-03-13
*	Removing Exc_located and using the new exception enrichement	ppedrot	2013-02-18
*	Revised the Ltac trace mechanism so that trace breaking due to	herbelin	2013-02-17
*	Modulification of identifier	ppedrot	2012-12-14
*	Monomorphization (proof)	ppedrot	2012-11-25
*	Monomorphized a lot of equalities over OCaml integers, thanks to	ppedrot	2012-11-08
*	remove Refiner.abstract_tactic and similar	letouzey	2012-10-06
*	Clean-up : removal of Proof_type.tactic_expr	letouzey	2012-10-06