From f8b5525eea31c226dfb2ebdc22be512f8af2ebbe Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 8 Apr 2009 17:23:13 +0000
Subject: Some dead code removal + cleanups

  This commit concerns about the first half of the useless code
  mentionned by Oug for coqtop (without plugins). For the moment,
  Oug is used in a mode where any elements mentionned in a .mli
  is considered to be precious. This already allows to detect and
  remove about 600 lines, and more is still to come.

  Among the interesting points, the type Entries.specification_entry
  and its constructors SPExxx were never used. Large parts of cases.ml
  (and hence subtac_cases.ml) were also useless.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12069 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/bigint.ml | 4 ----
 1 file changed, 4 deletions(-)

(limited to 'lib')

diff --git a/lib/bigint.ml b/lib/bigint.ml
index a836d0e073..3b974652b9 100644
--- a/lib/bigint.ml
+++ b/lib/bigint.ml
@@ -167,8 +167,6 @@ let less_than m n =
     (Array.length m = Array.length n && less_than_same_size m n 0 0))
 
 let equal m n = (m = n)
-  
-let less_or_equal_than m n = equal m n or less_than m n
 
 let less_than_shift_pos k m n =
   (Array.length m - k < Array.length n)
@@ -335,9 +333,7 @@ let one = big_of_int 1
 let sub_1 n = sub n one
 let add_1 n = add n one
 let two = big_of_int 2
-let neg_two = big_of_int (-2)
 let mult_2 n = add n n
-let is_zero n = n=zero
 
 let div2_with_rest n =
   let (q,b) = euclid n two in
-- 
cgit v1.2.3