diff options
| -rw-r--r-- | theories/NArith/BinNatDef.v | 4 | ||||
| -rw-r--r-- | theories/PArith/BinPosDef.v | 3 | ||||
| -rw-r--r-- | theories/ZArith/BinIntDef.v | 6 |
3 files changed, 1 insertions, 12 deletions
diff --git a/theories/NArith/BinNatDef.v b/theories/NArith/BinNatDef.v index d7660422a..b95c9b4bc 100644 --- a/theories/NArith/BinNatDef.v +++ b/theories/NArith/BinNatDef.v @@ -116,10 +116,6 @@ Infix "?=" := compare (at level 70, no associativity) : N_scope. (** Boolean equality and comparison *) -(** Nota: this [eqb] is not convertible with the generated [N_beq], - since the underlying [Pos.eqb] differs from [positive_beq] - (cf BinIntDef). *) - Fixpoint eqb n m := match n, m with | 0, 0 => true diff --git a/theories/PArith/BinPosDef.v b/theories/PArith/BinPosDef.v index 7916511a4..df125c684 100644 --- a/theories/PArith/BinPosDef.v +++ b/theories/PArith/BinPosDef.v @@ -288,9 +288,6 @@ Definition max p p' := (** ** Boolean equality and comparisons *) -(** Nota: this [eqb] is not convertible with the generated [positive_beq], due - to a different guard argument. We keep this version for compatibility. *) - Fixpoint eqb p q {struct q} := match p, q with | p~1, q~1 => eqb p q diff --git a/theories/ZArith/BinIntDef.v b/theories/ZArith/BinIntDef.v index d96d20fbb..c03b8517b 100644 --- a/theories/ZArith/BinIntDef.v +++ b/theories/ZArith/BinIntDef.v @@ -183,7 +183,7 @@ Definition ltb x y := (** Nota: [geb] and [gtb] are provided for compatibility, but [leb] and [ltb] should rather be used instead, since - more results we be available on them. *) + more results will be available on them. *) Definition geb x y := match x ?= y with @@ -197,10 +197,6 @@ Definition gtb x y := | _ => false end. -(** Nota: this [eqb] is not convertible with the generated [Z_beq], - since the underlying [Pos.eqb] differs from [positive_beq] - (cf BinIntDef). *) - Fixpoint eqb x y := match x, y with | 0, 0 => true |