From 58962f43da831ecb27d25703d52962599ea8ed23 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 30 May 2012 17:08:12 +0000
Subject: 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
---
 theories/PArith/BinPosDef.v | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'theories/PArith')

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
-- 
cgit v1.2.3