diff options
| author | letouzey | 2009-11-11 21:49:26 +0000 |
|---|---|---|
| committer | letouzey | 2009-11-11 21:49:26 +0000 |
| commit | 3e5b93760241671c8959da1cdb8023cfa7f62987 (patch) | |
| tree | c8f1d8b492b4efca26d9e442165b92532f34656c | |
| 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
| -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 898733bd87..a5f99cc66c 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 d29fb8f388..9540aace7f 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). |