diff options
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Lists/PolyList.v | 2 | ||||
| -rw-r--r-- | theories/Lists/PolyListSyntax.v | 5 | ||||
| -rw-r--r-- | theories/ZArith/Zdiv.v | 4 |
3 files changed, 6 insertions, 5 deletions
diff --git a/theories/Lists/PolyList.v b/theories/Lists/PolyList.v index 57ed3ec2d1..c007686caf 100644 --- a/theories/Lists/PolyList.v +++ b/theories/Lists/PolyList.v @@ -47,7 +47,7 @@ Fixpoint app [l:list] : list -> list end. Infix RIGHTA 7 "^" app : list_scope - V8only 45. + V8only RIGHTA 45. Lemma app_nil_end : (l:list)l=(l^nil). Proof. diff --git a/theories/Lists/PolyListSyntax.v b/theories/Lists/PolyListSyntax.v index b469b94f4f..e84398b517 100644 --- a/theories/Lists/PolyListSyntax.v +++ b/theories/Lists/PolyListSyntax.v @@ -14,5 +14,6 @@ Require PolyList. V8Infix "::" cons (at level 45, right associativity) : list_scope. -Infix RIGHTA 7 "^" app (* : list_scope *) - V8only 45. +Infix RIGHTA 7 "^" app : list_scope V8only RIGHTA 45. + +Open Scope list_scope. diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index eee40d6938..bcf5a05915 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -286,8 +286,8 @@ Syntax constr ]. -Infix 3 "/" Zdiv (no associativity) : Z_scope V8only (left associativity). -Infix 3 "mod" Zmod (no associativity) : Z_scope V8only (left associativity). +Infix 3 "/" Zdiv (no associativity) : Z_scope V8only. +Infix 3 "mod" Zmod (no associativity) : Z_scope. (** Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *) |