diff options
Diffstat (limited to 'theories/ZArith/Zdiv.v')
| -rw-r--r-- | theories/ZArith/Zdiv.v | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v index aa09915835..65b4422a11 100644 --- a/theories/ZArith/Zdiv.v +++ b/theories/ZArith/Zdiv.v @@ -288,10 +288,8 @@ Syntax constr -> [ (ZEXPR $n1):E " %" [1 0] (ZEXPR $n2):L ] . ]. -Infix 3 "/" Zdiv : Z_scope - V8only 30. -Infix 3 "mod" Zmod : Z_scope - V8only 30. +Infix 3 "/" Zdiv : Z_scope. +Infix 3 "mod" Zmod : Z_scope. (** Other lemmas (now using the syntax for [Zdiv] and [Zmod]). *) |