coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Making detyping potentially lazy.	Pierre-Marie Pédrot	2017-09-04
*	A new step of restructuration of notations.	Hugo Herbelin	2017-08-29
*	A little reorganization of notations + a fix to #5608.	Hugo Herbelin	2017-08-29
*	Merge PR #864: Some cleanups after cumulativity for inductive types	Maxime Dénès	2017-08-16
\|\
\| *	Improve errors for cumulativity when monomorphic	Amin Timany	2017-07-31
* \|	Adding support for recursive notations of the form "x , .. , y , z".	Hugo Herbelin	2017-07-26
\|/
*	Bump year in headers.	Pierre-Marie Pédrot	2017-07-04
*	[vernac] Remove stale bool parameter from `VernacStartTheoremProof`	Emilio Jesus Gallego Arias	2017-06-21
*	Merge PR#774: [ide] Add route_id parameter to query call.	Maxime Dénès	2017-06-20
\|\
\| *	[ide] Add route_id parameter to query call.	Emilio Jesus Gallego Arias	2017-06-18
* \|	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
\|/
*	Merge PR#719: Constrexpr.Numeral without bigint	Maxime Dénès	2017-06-15
\|\
* \	Merge PR#765: Remove obsolete Show commands	Maxime Dénès	2017-06-14
\|\ \
\| \| *	Constrexpr.Numeral stays uninterpreted (string+sign instead of BigInt.t)	Pierre Letouzey	2017-06-14
\| * \|	Remove Show Thesis command which was never implemented.	Théo Zimmermann	2017-06-12
\| * \|	Remove non-working Show Tree and Show Node commands.	Théo Zimmermann	2017-06-12
\| * \|	Remove Show Implicit Arguments command.	Théo Zimmermann	2017-06-12
\| \|/
* /	A fix to #5414 (ident bound by ltac names now known for "match").	Hugo Herbelin	2017-06-09
\|/
*	Put all plugins behind an "API".	Matej Kosik	2017-06-07
*	Remove the Sigma (monotonous state) API.	Maxime Dénès	2017-06-06
*	Merge PR#590: A more explicit algebraic type for evars of kind MatchingVar + ...	Maxime Dénès	2017-06-05
\|\
\| *	Using a more explicit algebraic type for evars of kind "MatchingVar".	Hugo Herbelin	2017-05-31
* \|	Support for using type information to infer more precise evar sources.	Hugo Herbelin	2017-05-30
\|/
*	[location] Renaming "CAst.ast" to "CAst.t"	Matej Košík	2017-05-24
*	Merge branch 'trunk' into located_switch	Emilio Jesus Gallego Arias	2017-05-24
\|\
\| *	[vernac] Remove `Save thm id.` command.	Emilio Jesus Gallego Arias	2017-05-23
\| *	[interp] [ast] Make raw_cases_pattern_expr private.	Emilio Jesus Gallego Arias	2017-05-15
\| *	Allow flexible anonymous universes in instances and sorts.	Gaetan Gilbert	2017-05-03
\| *	Merge PR#582: Fix warnings	Maxime Dénès	2017-05-02
\| \|\
\| * \|	Revert "Using a more explicit algebraic type for evars of kind "MatchingVar"."	Maxime Dénès	2017-04-28
\| * \|	Using a more explicit algebraic type for evars of kind "MatchingVar".	Hugo Herbelin	2017-04-28
\| * \|	Merge PR#531: Fixing bug #5420 and many similar bugs due to the presence of l...	Maxime Dénès	2017-04-28
\| \|\ \
\| \| \| *	Remove unused [open] statements	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] Be consistent with type module qualification	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] More located use.	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.predicate_pattern to 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
\|/ /
* \|	Remove VernacError	Gaetan Gilbert	2017-04-21
* \|	Merge PR#379: Introducing evar-insensitive constrs	Maxime Dénès	2017-04-11
\|\ \
\| \| *	Documenting how the recursive indices of a fixpoint are computed.	Hugo Herbelin	2017-04-09
\| \| *	Removing internal support for accepting "{struct x}" and co in "Theorem with".	Hugo Herbelin	2017-04-09
\| \|/ \|/\|
* \|	[camlpX] Remove camlp4 compat layer.	Emilio Jesus Gallego Arias	2017-04-07
\| *	Merge branch 'trunk' into pr379	Maxime Dénès	2017-04-04
\| \|\ \| \|/ \|/\|