From 6899d3aa567436784a08af4e179c2ef1fa504a02 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 21 Nov 2015 00:17:21 +0100
Subject: Moving extended_rel_vect/extended_rel_list to the kernel.

It will later be used to fix a bug and improve some code.

Interestingly, there were a redundant semantic equivalent to
extended_rel_list in the kernel called local_rels, and another private
copy of extended_rel_list in exactly the same file.
---
 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 cefb5eca54..466d487153 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -292,14 +292,6 @@ let is_primitive_record (mib,_) =
   | Some (Some _) -> true
   | _ -> false
 
-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 build_dependent_inductive ind (_,mip) params =
   let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
   applist
-- 
cgit v1.2.3