From bb7d7482724489521dde94a5b70af7864acfa802 Mon Sep 17 00:00:00 2001
From: barras
Date: Thu, 1 Mar 2001 10:09:34 +0000
Subject: nouvelle implantation de la reduction suppression de IsXtra du noyau

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

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 620f31eaa8..a5920f870c 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -345,14 +345,6 @@ let build_branch_type env dep p cs =
 
 (* [Rel (n+m);...;Rel(n+1)] *)
 
-let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i))
-
-let rel_list n m = 
-  let rec reln l p = 
-    if p>m then l else reln (mkRel(n+p)::l) (p+1)
-  in 
-  reln [] 1
-
 let extended_rel_list n hyps =
   let rec reln l p = function
     | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
-- 
cgit v1.2.3