From 8659ff43db85c43df644da6ac08509374aabcad4 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 11 Nov 2009 10:55:32 +0000 Subject: Improving abbreviations/notations + backtrack of semantic change in r12439 - Deactivation of short names registration and printing for abbreviations to identical names, what avoids printing uselessly qualified names binding where the short name is in fact equivalent. - New treatment of abbreviations to names: don't insert any maximally inserted implicit arguments at all at the time of the abbreviation and use the regular internalization strategy to have them inserted at use time. - The previous modifications altogether make redirections of qualified names easier and avoid the semantic change of r12349 and hence allows to keep "Notation b := @a" as it was before, i.e. as a notation for the deactivation of the implicit arguments of a. - Took benefit of these changes and updated nil/cons/list/app redefinition in "List.v". - Fixed parsing/printing notation bugs (loop on partially applied abreviations for constructors in constrintern.ml + bad reverting of notations with holes that captured non anonymous variables in match_cases_pattern). - Add support for parsing/printing abbreviations to @-like constructors and for reverting printing for abbreviations to constructors applied to parameters only (function extern_symbol_pattern). - Minor error messages fixes and minor APIs cleaning. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12494 85f007b7-540e-0410-9357-904b9bb8a0f7 --- test-suite/prerequisite/make_notation.v | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'test-suite/prerequisite') diff --git a/test-suite/prerequisite/make_notation.v b/test-suite/prerequisite/make_notation.v index 4a75713d1..c93d102a2 100644 --- a/test-suite/prerequisite/make_notation.v +++ b/test-suite/prerequisite/make_notation.v @@ -1,3 +1,8 @@ (* Used in Notation.v to test import of notations from files in sections *) Notation "'Z'" := O (at level 9). +Notation plus := plus. +Notation succ := S. +Notation mult := mult (only parsing). +Notation less := le (only parsing). + -- cgit v1.2.3