coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
...
*	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
\|\ \
* \| \|	[stm] Remove some obsolete vernacs/classification.	Emilio Jesus Gallego Arias	2017-03-24
\| * \|	Unifying standard "constr_level" names for constructors of local_binder_expr.	Hugo Herbelin	2017-03-24
\| * \|	"Standardizing" the name LocalPatten into LocalRawPattern.	Hugo Herbelin	2017-03-24
\|/ /
\| *	Factorizing/unifying code in dealing with binders.	Hugo Herbelin	2017-03-23
\|/
*	Merge branch 'v8.6'	Pierre-Marie Pédrot	2017-03-22
\|\
\| *	don't require printing-only notation to be productive	Ralf Jung	2017-02-16
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-30
\|\\|
\| *	Fix #5174: Underinformative syntax error messages in the new arguments syntax	Maxime Dénès	2016-11-30
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-11-18
\|\\|
\| *	Revert "Merge remote-tracking branch 'github/pr/360' into v8.6"	Maxime Dénès	2016-11-18
\| *	[stm] Remove STM-related vernaculars	Emilio Jesus Gallego Arias	2016-11-17
\| *	Merge remote-tracking branch 'github/pr/339' into v8.6	Maxime Dénès	2016-11-07
\| \|\
\| * \	Merge remote-tracking branch 'github/pr/340' into v8.6	Maxime Dénès	2016-11-03
\| \|\ \
\| \| \| *	Lets Hints/Instances take an optional pattern	Matthieu Sozeau	2016-11-03
\| * \| \|	Better Arguments compatibility.	Maxime Dénès	2016-11-02
\| \| \|/ \| \|/\|
\| \| *	Fix various shortcomings of the warnings infrastructure.	Maxime Dénès	2016-11-02
\| \|/
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-29
\|\\|
\| *	Complete overhaul of the Arguments vernacular.	Maxime Dénès	2016-10-27
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-08
\|\\|
\| *	Do not add "Append" as a lexer keyword.	Pierre-Marie Pédrot	2016-10-06
* \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-05
\|\\|
\| *	Revert "Move bullet detection from lexer to parser (bug #5102)."	Guillaume Melquiond	2016-10-05
\| *	Merge remote-tracking branch 'github/pr/305' into v8.6	Maxime Dénès	2016-10-04
\| \|\
* \| \|	Merge branch 'v8.6'	Pierre-Marie Pédrot	2016-10-02
\|\\| \|
\| * \|	Move bullet detection from lexer to parser (bug #5102).	Guillaume Melquiond	2016-10-02