Fixed my last patch: these files no longer use nat_beq (automatically

generated) but rather use beq_nat (Arith.EqNat)



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14126 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 5 insertions, 4 deletions

diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
index 3f8e84ecd..0a303b63f 100644
--- a/plugins/extraction/ExtrOcamlNatBigInt.v
+++ b/plugins/extraction/ExtrOcamlNatBigInt.v
@@ -36,7 +36,7 @@ Extract Constant pred => "fun n -> Big.max Big.zero (Big.pred n)".
 Extract Constant minus => "fun n m -> Big.max Big.zero (Big.sub n m)".
 Extract Constant max => "Big.max".
 Extract Constant min => "Big.min".
-Extract Constant nat_beq => "Big.eq".
+(*Extract Constant nat_beq => "Big.eq".*)
 Extract Constant EqNat.beq_nat => "Big.eq".
 Extract Constant EqNat.eq_nat_decide => "Big.eq".
 
diff --git a/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index f69fca984..a0cb26b5d 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -45,7 +45,7 @@ Extract Constant minus => "fun n m -> max 0 (n-m)".
 Extract Constant mult => "( * )".
 Extract Inlined Constant max => max.
 Extract Inlined Constant min => min.
-Extract Inlined Constant nat_beq => "(=)".
+(*Extract Inlined Constant nat_beq => "(=)".*)
 Extract Inlined Constant EqNat.beq_nat => "(=)".
 Extract Inlined Constant EqNat.eq_nat_decide => "(=)".
 
@@ -72,4 +72,4 @@ Definition test n m (H:m>0) :=
  nat_compare n (q*m+r).
 
 Recursive Extraction test fact.
-*)
\ No newline at end of file
+*)
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index e3e9078e3..b34cf338b 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -8,6 +8,7 @@
 
 Require Export List.
 Require Export BinPos.
+Require Arith.EqNat.
 
 Open Scope positive_scope.
 
@@ -59,7 +60,7 @@ simpl;auto.
 Qed.
 
 Lemma Lget_app : forall (A:Set) (a:A) l i,
-Lget i (l ++ a :: nil) = if nat_beq i (length l) then Some a else Lget i l.
+Lget i (l ++ a :: nil) = if Arith.EqNat.beq_nat i (length l) then Some a else Lget i l.
 Proof.
 induction l;simpl Lget;simpl length.
 intros [ | i];simpl;reflexivity.