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

2 files changed, 3 insertions, 3 deletions

diff --git a/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
index 3f8e84ecda..0a303b63fc 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 f69fca984a..a0cb26b5d3 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
+*)