coq - The formal proof system

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