coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-07-04
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	[vernac] Remove forward hooks from Obligations.	Emilio Jesus Gallego Arias	2017-06-20
*	[vernac] Remove unused hooks.	Emilio Jesus Gallego Arias	2017-06-20
*	Clean up universes of constants and inductives	Amin Timany	2017-06-16
*	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
*	Fix bugs	Amin Timany	2017-06-16
*	Squashed commit of the following:	Amin Timany	2017-06-16
*	Change the place of inference after sect discharge	Amin Timany	2017-06-16
*	Subtyping inference for inductoves and records	Amin Timany	2017-06-16
*	Add subtyping inference for inductive types	Amin Timany	2017-06-16
*	Using UInfoInd for universes in inductive types	Amin Timany	2017-06-16
*	Extend definition of inductives to include subtyping info	Amin Timany	2017-06-16
*	[proof] Deprecate redundant wrappers.	Emilio Jesus Gallego Arias	2017-06-11
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	Merge PR#662: Fixing bug #5233 and another bug with implicit arguments + a sh...	Maxime Dénès	2017-06-06
\|\
* \|	Drop '.' from CErrors.anomaly, insert it in args	Jason Gross	2017-06-02
* \|	Merge PR#696: Trunk+cleanup constr of global	Maxime Dénès	2017-06-01
\|\ \
* \ \	Merge PR#561: Improving the Name API	Maxime Dénès	2017-06-01
\|\ \ \
\| * \| \|	Creating a module Nameops.Name extending module Names.Name.	Hugo Herbelin	2017-05-31
\| \| \| *	More precise on preventing clash between bound vars name and hidden impargs.	Hugo Herbelin	2017-05-31
\| \| \| *	Fixing a failure to interpret some local implicit arguments in Inductive.	Hugo Herbelin	2017-05-31
\| \| \|/ \| \|/\|
* / \|	Support for using type information to infer more precise evar sources.	Hugo Herbelin	2017-05-30
\|/ /
\| *	Command.ml cleanup: remove constr_of_global calls	Matthieu Sozeau	2017-05-29
\|/
*	Merge PR#512: [cleanup] Unify all calls to the error function.	Maxime Dénès	2017-05-29
\|\
\| *	[cleanup] Unify all calls to the error function.	Emilio Jesus Gallego Arias	2017-05-27
* \|	[coqlib] Deprecate redundant Coqlib functions.	Emilio Jesus Gallego Arias	2017-05-27
\|/
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	Merge PR#582: Fix warnings	Maxime Dénès	2017-05-02
\| \|\
\| * \	Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...	Maxime Dénès	2017-04-28
\| \|\ \
\| \| \| *	Fix omitted labels in function calls	Gaetan Gilbert	2017-04-27
\| \| \|/ \| \|/\|
* \| \|	[location] [ast] Port module AST to CAst	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] [ast] Switch Constrexpr AST to an extensible node type.	Emilio Jesus Gallego Arias	2017-04-25
* \| \|	[location] Make location optional in Loc.located	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
* \| \|	[location] Use Loc.located for constr_expr.	Emilio Jesus Gallego Arias	2017-04-24
\| * \|	Removing tactic compatibility layer in Command.	Pierre-Marie Pédrot	2017-04-24
\|/ /
* \|	[flags] Deprecate is_silent/is_verbose in favor of single flag.	Emilio Jesus Gallego Arias	2017-04-21
* \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-04-15
* \|	Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...	Maxime Dénès	2017-04-12
\|\ \
\| \| *	Fixing #5420 as well as many related bugs due to miscounting let-ins.	Hugo Herbelin	2017-04-09
\| \| *	Fixing several wrong computations of implicit arguments by position	Hugo Herbelin	2017-04-09
\| \| *	Minor cosmetic commit.	Hugo Herbelin	2017-04-09
* \| \|	Merge branch 'master' into econstr	Pierre-Marie Pédrot	2017-04-07
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Merge PR#508: Optimize pending evars	Maxime Dénès	2017-04-06
\| \|\ \
* \| \| \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\|\\| \| \|
* \| \| \|	Actually exporting delayed universes in the EConstr implementation.	Pierre-Marie Pédrot	2017-04-01
* \| \| \|	Merge branch 'trunk' into pr379	Maxime Dénès	2017-03-24
\| * \| \|	Replacing "cast surgery" in LetIn by a proper field (see PR #404).	Hugo Herbelin	2017-03-24