diff options
Diffstat (limited to 'theories/ZArith/BinIntDef.v')
| -rw-r--r-- | theories/ZArith/BinIntDef.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index 55b9ec4a44..c05ed9ebf4 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -208,7 +208,7 @@ Definition gtb x y := | _ => false end. -Fixpoint eqb x y := +Definition eqb x y := match x, y with | 0, 0 => true | pos p, pos q => Pos.eqb p q |