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/ExtrOcamlNatInt.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/extraction/ExtrOcamlNatInt.v')

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