diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-30 17:08:12 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-30 17:08:12 +0000 |
commit | 58962f43da831ecb27d25703d52962599ea8ed23 (patch) | |
tree | 3489e109d8f160d318b40b3c6c39630d533d402a /theories/ZArith | |
parent | 1a09d9d0635ebd5f5be5f4165438db9122278fd2 (diff) |
Functions *_beq aren't generated anymore, remove comments about them
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15402 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/ZArith')
-rw-r--r-- | theories/ZArith/BinIntDef.v | 6 |
1 files changed, 1 insertions, 5 deletions
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 |