aboutsummaryrefslogtreecommitdiff
path: root/test-suite/success/Notations.v
AgeCommit message (Expand)Author
2017-11-27Fixing associativity registered for level 10.Hugo Herbelin
2017-10-19Moving bug numbers to BZ# format in the test-suite.Théo Zimmermann
2017-09-12Fixing little inaccuracy in coercions to ident or name.Hugo Herbelin
2017-04-06Merge branch 'origin/v8.5' into v8.6.Hugo Herbelin
2017-02-23Fixing a little bug in using the "where" clause for inductive types.Hugo Herbelin
2017-02-16reject notations that are both 'only printing' and 'only parsing'Ralf Jung
2017-02-16don't require printing-only notation to be productiveRalf Jung
2016-10-24Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-24Merge branch 'v8.5' into v8.6Hugo Herbelin
2016-10-24Fixing #3479 (parsing of "{" and "}" when a keyword starts with "{" or "}").Hugo Herbelin
2016-10-12Fixing a collision about the meta-variable ".." in recursive notations.Hugo Herbelin
2016-09-29Move vector/list compat notations to their relevant filesJason Gross
2016-07-16Fixing a collision about the meta-variable ".." in recursive notations.Hugo Herbelin
2015-11-26Fixing the "parsing rules with idents later declared as keywords" problem.Hugo Herbelin
2012-07-21Improving management of notations with binders (see #2708 where aherbelin
2012-03-23Fix the test-suite by removing any Reset in the scriptsletouzey
2012-03-20Fixing bug #2724 (using notations with binders in cases patternsherbelin
2011-12-18Fixing bug #2634 (unscoped notations were disturbing theherbelin
2011-12-07Fixing grammar resetting bug in the presence of levels initially emptyherbelin
2011-03-16Remove some weird syntax "fun ... ," that used to be accepted (cf r13876)letouzey
2010-12-04Fixing bug #2448 (wrongly-scoped alpha-renaming in notations).herbelin
2010-03-23Added automatic expansion on the left of recursive notationsherbelin
2009-11-11Improving abbreviations/notations + backtrack of semantic change in r12439herbelin
2009-10-28Made that notations to names behave like the names they refer to wrtherbelin
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-10-17Fixed a notation bug when extending binder_constr with empty levelsherbelin
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-04-08- Backport of 12053 (fixing parsing segfault bug #2087) and 12058 (fixingherbelin
2009-01-18Backporting from v8.2 to trunk:herbelin
2009-01-13- Standardized prefix use of "Local"/"Global" modifiers as decided inherbelin
2008-12-02Add new directory for pre-compilation of files needed for further tests.herbelin
2008-07-11Correction d'un autre bug autour de la gestion des niveaux vides deherbelin
2008-05-26Résolution bug #1850 sur notations avec niveaux inconnus deherbelin
2006-04-15Tests notationsherbelin