From befdbea90f91f85482c14a78120cf94b5bb0b5ea Mon Sep 17 00:00:00 2001
From: vsiles
Date: Mon, 16 May 2011 12:57:44 +0000
Subject: 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
---
 plugins/extraction/ExtrOcamlNatBigInt.v | 2 +-
 plugins/extraction/ExtrOcamlNatInt.v    | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/extraction')

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