diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-11 21:49:26 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-11-11 21:49:26 +0000 |
| commit | 3e5b93760241671c8959da1cdb8023cfa7f62987 (patch) | |
| tree | c8f1d8b492b4efca26d9e442165b92532f34656c /theories/NArith | |
| parent | 0601db38b579513e4ab39a161591cd359260490e (diff) | |
Better compatibility for Peqb
As show by contrib TreeAutomata, the Peqb now placed in BinPos
was using 1st arg as "struct", instead of 2nd arg as earlier.
Fix that, and remove the "Import BinPos BinNat" hack in Ndec
(merci Hugo :-).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12503 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/NArith')
| -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). |