coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	[coqlib] Deprecate redundant Coqlib functions.	Emilio Jesus Gallego Arias	2017-05-27
*	Merge PR#481: [option] Remove support for non-synchronous options.	Maxime Dénès	2017-05-25
\|\
* \	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\ \
\| \| *	[option] Remove support for non-synchronous options.	Emilio Jesus Gallego Arias	2017-05-24
\| \|/
\| *	Fix 4.04 warnings	Gaetan Gilbert	2017-04-27
\| *	Remove unused [open] statements	Gaetan Gilbert	2017-04-27
* \|	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias	2017-04-25
* \|	[location] Remove Loc.ghost.	Emilio Jesus Gallego Arias	2017-04-25
* \|	[location] Switch glob_constr to Loc.located	Emilio Jesus Gallego Arias	2017-04-24
\|/
*	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
* \| \|	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