diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-19 11:36:27 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-06-19 11:36:27 +0000 |
| commit | 826215450c44bb575e6ed2ab2ea8818131b996f4 (patch) | |
| tree | d0b0b8b8c8762ef7f2aff9f8c89175af1053d045 /theories/ZArith | |
| parent | 0908dac05b719cbc5d6fccdc7d71a82b82a06cea (diff) | |
BinInt: a forgotten scope for a notation
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15450 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith')
| -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 3a5eb8855..f3f7b850e 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. |