coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Change references to CAMLP4 to CAMLP5 to be more accurate since we no	Jim Fehrle	2018-02-17
*	[vernac] Mutual theorems (VernacStartTheoremProof) always have names	Vincent Laporte	2018-02-01
*	[vernac] Remove VernacGoal, allow anonymous definitions in VernacDefinition	Vincent Laporte	2018-02-01
*	[vernac] vernac_expr no longer recursive	Vincent Laporte	2018-01-08
*	Merge PR #6433: [flags] Move global time flag into an attribute.	Maxime Dénès	2017-12-29
\|\
* \|	[api] Also deprecate constructors of Decl_kinds.	Emilio Jesus Gallego Arias	2017-12-23
\| *	[flags] Move global time flag into an attribute.	Emilio Jesus Gallego Arias	2017-12-23
\|/
*	Separate vernac controls and regular commands.	Maxime Dénès	2017-12-20
*	Remove "obsolete_locality" and fix STM vernac classification.	Maxime Dénès	2017-11-29
*	Allow local universe renaming in Print.	Gaëtan Gilbert	2017-11-25
*	Merge PR #6200: Remove pidentref grammar entry.	Maxime Dénès	2017-11-23
\|\
\| *	Remove pidentref grammar entry.	Gaëtan Gilbert	2017-11-20
* \|	[parser] Remove unnecessary statically initialized hook.	Emilio Jesus Gallego Arias	2017-11-19
\|/
*	Parse [Proof using Type] without translating Type to an id.	Gaëtan Gilbert	2017-10-10
*	Implementing a generic mechanism for locating named objects from Coq side.	Pierre-Marie Pédrot	2017-10-03
*	Efficient fresh name generation relying on sets.	Pierre-Marie Pédrot	2017-09-28
*	Merge PR #688: Binding universe constraints in Definition/Inductive/etc...	Maxime Dénès	2017-09-26
\|\
* \|	Remove STM vernaculars.	Maxime Dénès	2017-09-19
\| *	Allow declaring universe binders with no constraints with @{\|}	Gaëtan Gilbert	2017-09-19
\| *	Allow declaring universe constraints at definition level.	Matthieu Sozeau	2017-09-19
\|/
*	Merge PR #939: [general] Merge parsing with highparsing, put toplevel at the ...	Maxime Dénès	2017-09-15
\|\
* \	Merge PR #1037: Parse directly to Sorts.family when appropriate.	Maxime Dénès	2017-09-15
\|\ \
\| * \|	Parse directly to Sorts.family when appropriate.	Gaëtan Gilbert	2017-09-08
\| \| *	[vernac] Store Infix Modifier in Vernac Notation.	Pierre-Marie Pédrot	2017-08-29
\| \|/ \|/\|
* \|	[parsing] Remove hacks for reduced Prelude.	Emilio Jesus Gallego Arias	2017-08-29
\|/
*	Merge PR #937: [general] Remove spurious dependency of highparsing on toplevel.	Maxime Dénès	2017-08-29
\|\
* \|	Improve errors for cumulativity when monomorphic	Amin Timany	2017-07-31
* \|	Change the option for cumulativity	Amin Timany	2017-07-31
\| *	[general] Remove spurious dependency of highparsing on toplevel.	Emilio Jesus Gallego Arias	2017-07-31
\|/
*	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
*	Change the option to Set Inductive Cumulativity	Amin Timany	2017-06-16
*	Fix bugs and add an option for cumulativity	Amin Timany	2017-06-16
*	Grammar hacks to get nice errors about non-loaded plugins (extr,recdef)	Pierre Letouzey	2017-06-14
*	[cleanup] Unify all calls to the error function.	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
\| \|\ \
\| \| \| *	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 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#422: Supporting all kinds of binders, including 'pat, in syntax of r...	Maxime Dénès	2017-04-12
\|\ \
\| \| *	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 PR#417: No cast surgery in let in	Maxime Dénès	2017-04-03
\|\ \