coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	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] Move `Coqlib` to `library/`.	Emilio Jesus Gallego Arias	2017-05-27
* \|	[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
\| *	Remove some unused values and types	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] Use located in misctypes.	Emilio Jesus Gallego Arias	2017-04-24
* \|	[location] Switch glob_constr to Loc.located	Emilio Jesus Gallego Arias	2017-04-24
* \|	[location] Move Glob_term.cases_pattern to located.	Emilio Jesus Gallego Arias	2017-04-24
* \|	[location] Use Loc.located for constr_expr.	Emilio Jesus Gallego Arias	2017-04-24
* \|	[constrexpr] Make patterns use Loc.located for location information	Emilio Jesus Gallego Arias	2017-04-24
\|/
*	Merge PR#579: [flags] Deprecate is_silent/is_verbose in favor of single flag.	Maxime Dénès	2017-04-24
\|\
* \	Merge branch v8.6 into trunk	Hugo Herbelin	2017-04-22
\|\ \
\| \| *	[flags] Deprecate is_silent/is_verbose in favor of single flag.	Emilio Jesus Gallego Arias	2017-04-21
\| \|/ \|/\|
* \|	Merge PR#422: Supporting all kinds of binders, including 'pat, in syntax of r...	Maxime Dénès	2017-04-12
\|\ \
* \ \	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès	2017-04-11
\|\ \ \
* \| \| \|	[camlpX] Remove camlp4 compat layer.	Emilio Jesus Gallego Arias	2017-04-07
\| \| \| *	end of correction of bug 4306	Julien Forest	2017-04-04
\| \| \| *	Bad correction in previous commit	Julien Forest	2017-04-04
\| \| \| *	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
\| \|\ \ \ \| \|/ / / \|/\| \| \|
\| * \| \|	Using delayed universe instances in EConstr.	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
* \| \| \| \|	Unifying standard "constr_level" names for constructors of local_binder_expr.	Hugo Herbelin	2017-03-24
* \| \| \| \|	Renaming local_binder into local_binder_expr.	Hugo Herbelin	2017-03-24
* \| \| \| \|	"Standardizing" the name LocalPatten into LocalRawPattern.	Hugo Herbelin	2017-03-24
\| \|/ / / \|/\| \| \|
\| \| * \|	Improving the API of constrexpr_ops.mli.	Hugo Herbelin	2017-03-23
\| \|/ / \|/\| \|
* \| \|	Revert "Add empty Extraction.v and FunInd.v to prepare landing of PR#220."	Maxime Dénès	2017-03-23
* \| \|	Merge branch 'v8.6' into trunk	Maxime Dénès	2017-03-23
\|\ \ \ \| \| \|/ \| \|/\|
\| * \|	Merge PR#495: funind: Ignore missing info for current function	Maxime Dénès	2017-03-23
\| \|\ \
\| * \| \|	Add empty Extraction.v and FunInd.v to prepare landing of PR#220.	Maxime Dénès	2017-03-23
\| \| * \|	funind: Ignore missing info for current function	Tej Chajed	2017-03-22
\| \|/ /
* \| \|	Moving the Ltac plugin to a pack-based one.	Pierre-Marie Pédrot	2017-02-17
\| \| *	Merge branch 'master'.	Pierre-Marie Pédrot	2017-02-14
\| \| \|\ \| \|_\|/ \|/\| \|
\| \| *	Namegen primitives now apply on evar constrs.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Definining EConstr-based contexts.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Evar-normalizing functions now act on EConstrs.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Removing various compatibility layers of tactics.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Funind API using EConstr.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Ltac now uses evar-based constrs.	Pierre-Marie Pédrot	2017-02-14
\| \| *	Removing compatibility layers in Retyping	Pierre-Marie Pédrot	2017-02-14