From 5c1768a4dcf39ffd7d58ea9448a842376e86ccf9 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 5 Mar 2001 08:20:05 +0000
Subject: Re-Déplacement extended_rel_list

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

(limited to 'kernel/inductive.ml')

diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index a5920f870c..f03b1ba14f 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -343,14 +343,3 @@ let build_branch_type env dep p cs =
   else
     it_mkProd_or_LetIn base cs.cs_args
 
-(* [Rel (n+m);...;Rel(n+1)] *)
-
-let extended_rel_list n hyps =
-  let rec reln l p = function
-    | (_,None,_) :: hyps -> reln (mkRel (n+p) :: l) (p+1) hyps
-    | (_,Some _,_) :: hyps -> reln l (p+1) hyps
-    | [] -> l
-  in 
-  reln [] 1 hyps
-
-let extended_rel_vect n hyps = Array.of_list (extended_rel_list n hyps)
-- 
cgit v1.2.3