From abf06dadb072b3b8eb0488ce1c72b22bd802b116 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Wed, 6 Sep 2006 13:10:00 +0000
Subject: Definition redondante

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@78 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 caml/Camlcoq.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'caml/Camlcoq.ml')

diff --git a/caml/Camlcoq.ml b/caml/Camlcoq.ml
index fc5d2d87..b0bb4ff9 100644
--- a/caml/Camlcoq.ml
+++ b/caml/Camlcoq.ml
@@ -7,11 +7,6 @@ open BinInt
 
 (* Integers *)
 
-let rec camlint_of_nat n =
-  match n with
-  | O -> 0l
-  | S n -> Int32.add (camlint_of_nat n) 1l
-
 let rec camlint_of_positive = function
   | Coq_xI p -> Int32.add (Int32.shift_left (camlint_of_positive p) 1) 1l
   | Coq_xO p -> Int32.shift_left (camlint_of_positive p) 1
-- 
cgit