coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Remove reference name type.	Maxime Dénès	2018-06-18
*	[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.	Emilio Jesus Gallego Arias	2018-05-04
*	[api] Move structures deprecated in the API to the core.	Emilio Jesus Gallego Arias	2017-11-06
*	[stm] Remove state-handling from Futures.	Emilio Jesus Gallego Arias	2017-10-17
*	deprecate Pp.std_ppcmds type alias	Matej Košík	2017-07-27
*	[API] Remove `open API` in ml files in favor of `-open API` flag.	Emilio Jesus Gallego Arias	2017-07-17
*	Removing Proof_type from the API.	Pierre-Marie Pédrot	2017-06-16
*	Remove (useless) aliases from the API.	Matej Košík	2017-06-10
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Merge branch v8.6 into trunk	Hugo Herbelin	2017-04-22
\|\
\| *	Solving first problem in bug #4306. TO DO : solve the let in problem	Julien Forest	2017-04-04
* \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\|\ \
\| * \|	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24
\| \|/
* /	Funind API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\|/
*	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
*	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
*	This commit adds full universe polymorphism and fast projections to Coq.	Matthieu Sozeau	2014-05-06
*	Factoring(continued).	Arnaud Spiwack	2013-12-04
*	The commands that initiate proofs are now in charge of what happens when proo...	Arnaud Spiwack	2013-12-04
*	declaration_hooks use Ephemeron	gareuselesinge	2013-10-18
*	invalid_arg instead of raise (Invalid_argement ...)	letouzey	2013-03-12
*	Modulification of name	ppedrot	2012-12-18
*	Modulification of identifier	ppedrot	2012-12-14
*	global_reference migrated from Libnames to new Globnames, less deps in gramma...	letouzey	2012-05-29
*	Final part of moving Program code inside the main code. Adapted add_definitio...	msozeau	2012-03-14
*	New version of recdef :	jforest	2012-03-01
*	Rename rawterm.ml into glob_term.ml	glondu	2010-12-23
*	Change of nomenclature: rawconstr -> glob_constr	glondu	2010-12-23
*	Here comes the commit, announced long ago, of the new tactic engine.	aspiwack	2010-04-22
*	adding an option functional_induction_rewrite_dependent to make functional in...	jforest	2009-12-16
*	Delete trailing whitespaces in all .{v,ml} files	glondu	2009-09-17
*	Directory 'contrib' renamed into 'plugins', to end confusion with archive of ...	letouzey	2009-03-20