diff options
| -rw-r--r-- | theories/NArith/BinPos.v | 2 | ||||
| -rw-r--r-- | theories/NArith/Ndec.v | 6 |
2 files changed, 3 insertions, 5 deletions
diff --git a/theories/NArith/BinPos.v b/theories/NArith/BinPos.v index 898733bd8..a5f99cc66 100644 --- a/theories/NArith/BinPos.v +++ b/theories/NArith/BinPos.v @@ -269,7 +269,7 @@ Definition Pmax (p p' : positive) := match Pcompare p p' Eq with (********************************************************************) (** Boolean equality *) -Fixpoint Peqb (x y : positive) : bool := +Fixpoint Peqb (x y : positive) {struct y} : bool := match x, y with | 1, 1 => true | p~1, q~1 => Peqb p q diff --git a/theories/NArith/Ndec.v b/theories/NArith/Ndec.v index d29fb8f38..9540aace7 100644 --- a/theories/NArith/Ndec.v +++ b/theories/NArith/Ndec.v @@ -19,10 +19,8 @@ Require Import Ndigits. (** A boolean equality over [N] *) -Notation Peqb := BinPos.Peqb (only parsing). -Notation Neqb := BinNat.Neqb (only parsing). - -Import BinPos BinNat. +Notation Peqb := Peqb (only parsing). (* Now in [BinPos] *) +Notation Neqb := Neqb (only parsing). (* Now in [BinNat] *) Notation Peqb_correct := Peqb_refl (only parsing). |