diff options
Diffstat (limited to 'theories/Lists/PolyListSyntax.v')
| -rw-r--r-- | theories/Lists/PolyListSyntax.v | 9 |
1 files changed, 0 insertions, 9 deletions
diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v index 640cf3fbfe..a4b6a57aae 100644 --- a/theories/Lists/PolyListSyntax.v +++ b/theories/Lists/PolyListSyntax.v @@ -8,12 +8,3 @@ (*i $Id$ i*) -(** Syntax for list concatenation *) - -Require PolyList. - -V8Infix "::" cons (at level 45, right associativity) : list_scope. - -Infix RIGHTA 7 "^" app : list_scope V8only RIGHTA 45 "++". - -Open Scope list_scope. |