diff options
| -rw-r--r-- | theories/Lists/PolyList.v | 9 | ||||
| -rw-r--r-- | theories/Lists/PolyListSyntax.v | 7 |
2 files changed, 12 insertions, 4 deletions
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index cdc0f36553..57ed3ec2d1 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -22,6 +22,11 @@ Inductive list : Set := nil : list | cons : A -> list -> list. Unset Contextual Implicits. +Infix "::" cons (at level 7, right associativity) : list_scope + V8only (at level 45, right associativity). + +Open Scope list_scope. + (*************************) (** Discrimination *) (*************************) @@ -41,8 +46,8 @@ Fixpoint app [l:list] : list -> list | (cons a l1) => (cons a (app l1 m)) end. -Infix RIGHTA 7 "^" app - V8only 30. +Infix RIGHTA 7 "^" app : list_scope + V8only 45. Lemma app_nil_end : (l:list)l=(l^nil). Proof. diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v index b74da123fb..be23cd6655 100644 --- a/theories/Lists/PolyListSyntax.v +++ b/theories/Lists/PolyListSyntax.v @@ -12,5 +12,8 @@ Require PolyList. -Infix RIGHTA 7 "^" app - V8only 30. +Infix "::" cons (at level 7, right associativity) : list_scope + V8only (at level 45). + +Infix RIGHTA 7 "^" app (* : list_scope *) + V8only 45. |