diff options
| -rw-r--r-- | theories/ZArith/BinInt.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/BinInt.v b/theories/ZArith/BinInt.v index 3a5eb8855e..f3f7b850ee 100644 --- a/theories/ZArith/BinInt.v +++ b/theories/ZArith/BinInt.v @@ -1353,7 +1353,7 @@ Infix "mod" := Z.modulo (at level 40, no associativity) : Z_scope. Infix "รท" := Z.quot (at level 40, left associativity) : Z_scope. (* TODO : transition from Zdivide *) -Notation "( x | y )" := (Z.divide x y) (at level 0). +Notation "( x | y )" := (Z.divide x y) (at level 0) : Z_scope. Infix "?=" := Z.compare (at level 70, no associativity) : Z_scope. |