coq - the Coq proof assistant

	Commit message (Expand)	Author	Age
*	Revert "Merge PR #873: New strategy based on open scopes for deciding which n...	Maxime Dénès	2018-03-09
*	Supporting recursive notations reversing the left-to-right order.	Hugo Herbelin	2018-02-20
*	Selecting which notation to print based on current stack of scope.	Hugo Herbelin	2017-11-27
*	Fixing bug #5693 (treating empty notation format as any format).	Hugo Herbelin	2017-09-12
*	[pp] Make feedback the only logging mechanism.	Emilio Jesus Gallego Arias	2017-03-21
*	Do not give a name to anonymous evars anymore. See bug #4547.	Pierre-Marie Pédrot	2016-02-13
*	Fix test-suite after 1343b69221ce3eeb3154732e73bbdc0044b224a8.	Maxime Dénès	2015-06-24
*	Fix testsuite with respect to the new formatting of Fail messages.	Guillaume Melquiond	2015-03-05
*	Fixing name of evars in output test Notation.v.	Hugo Herbelin	2015-01-12
*	Fixing typo in output test Notations.	Hugo Herbelin	2014-10-22
*	Adapting output tests to the removal of the new token warning and to	Hugo Herbelin	2014-10-21
*	Adapting the output test Notations:	Hugo Herbelin	2014-10-02
*	test-suite/output/Notations : evar number change	Pierre Boutillier	2013-12-19
*	Test suite: update output reference.	xclerc	2013-12-02
*	Updating some output tests in test-suite:	herbelin	2013-05-09
*	Using Parameter instead of Variable in test-suite/output	herbelin	2013-04-17
*	Fixing parsing of specific primitive tokens used as notations for patterns	herbelin	2012-12-18
*	Revised the strategy for automatic insertion of spaces when printing	herbelin	2012-12-04
*	Fixing bug #2835 (the rationale for printing notations was not	herbelin	2012-07-21
*	Constrextern is allow to use partially applied notations	pboutill	2012-06-14
*	Parameters in pattern first step.	pboutill	2012-01-16
*	Fix test-suite for s/Defining '\1' as keyword/Identifier '\1' now a keyword/.	letouzey	2011-09-22
*	Partly revert commit r14389 about relaxing the condition for being a keyword	herbelin	2011-08-10
*	Be a bit less aggressive in declaring idents as keywords in notations	herbelin	2011-08-08
*	Make Notation works with anonymous-level "Type".	herbelin	2011-06-08
*	Extension of the recursive notations mechanism	herbelin	2010-07-22
*	Backported r13068 to branch v8.3 (whd_betaiota on inferred return	herbelin	2010-06-04
*	Improving abbreviations/notations + backtrack of semantic change in r12439	herbelin	2009-11-11
*	Miscellaneous fixes and improvements:	herbelin	2008-12-02
*	- Ajout possibilité de lancer ocamldebug sur coqide	herbelin	2008-11-07
*	Affichage des notations récursives:	herbelin	2008-10-22
*	Prise en compte réversibilité des notations de la forme "Notation Nil := @n...	herbelin	2007-05-10
*	Exemple avec liaison des variables de filtrage du match	herbelin	2006-10-09
*	Notations:	herbelin	2006-10-09
*	Correction bug #1179 (result of Notation.decompose_notation_key in wrong order	herbelin	2006-09-23
*	- Correction filtrage des notations impliquant un "match" : la présence	herbelin	2006-09-23
*	Ajout test notation récursive	herbelin	2006-01-11
*	Test choix conflit afficheur de nombres selon la présence ou pas d'une coercion	herbelin	2006-01-05
*	Abandon tests syntaxe v7; remplacement des .v par des fichiers en syntaxe v8	herbelin	2005-12-22
*	Ajout suffixe 8 pour test en nouvelle syntaxe	herbelin	2004-12-09
*	Test lieurs dans Notation	herbelin	2004-11-17