diff options
Diffstat (limited to 'theories/PArith')
| -rw-r--r-- | theories/PArith/BinPosDef.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 22f3dcd64..fe1ec9398 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -268,7 +268,7 @@ Fixpoint compare_cont (r:comparison) (x y:positive) {struct y} : comparison := | 1, 1 => r end. -Definition compare x y := compare_cont Eq x y. +Definition compare := compare_cont Eq. Infix "?=" := compare (at level 70, no associativity) : positive_scope. |