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.

3 files changed, 28 insertions, 8 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index 796f06d37e..5923048fa4 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -111,6 +111,20 @@ let instance_from_named_context sign =
   in
   List.map_filter filter sign
 
+(** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
+   with n = |Δ| and with the local definitions of [Γ] skipped in
+   [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+
+let extended_rel_list n hyps =
+  let rec reln l p = function
+  | (_, None, _) :: hyps -> reln (Constr.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)
+
 let fold_named_context f l ~init = List.fold_right f l init
 let fold_named_list_context f l ~init = List.fold_right f l init
 let fold_named_context_reverse f ~init l = List.fold_left f init l
diff --git a/kernel/context.mli b/kernel/context.mli
index 5279aefb6b..7354677474 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -82,8 +82,21 @@ val fold_named_context_reverse :
   ('a -> named_declaration -> 'a) -> init:'a -> named_context -> 'a
 
 (** {6 Section-related auxiliary functions } *)
+
+(** [instance_from_named_context Ω] builds an instance [args] such
+    that [Ω ⊢ args:Ω] where [Ω] is a named context and with the local
+    definitions of [Ω] skipped. Example: for [id1:T,id2:=c,id3:U], it
+    gives [Var id1, Var id3]. All [idj] are supposed distinct. *)
 val instance_from_named_context : named_context -> Constr.t list
 
+(** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
+   with n = |Δ| and with the local definitions of [Γ] skipped in
+   [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+val extended_rel_list : int -> rel_context -> Constr.t list
+
+(** [extended_rel_vect n Γ] does the same, returning instead an array. *)
+val extended_rel_vect : int -> rel_context -> Constr.t array
+
 (** {6 ... } *)
 (** Signatures of ordered optionally named variables, intended to be
    accessed by de Bruijn indices *)
@@ -120,3 +133,4 @@ val rel_context_length : rel_context -> int
 val rel_context_nhyps : rel_context -> int
 (** Indicates whether a LetIn or a Lambda, starting from oldest declaration *)
 val rel_context_tags : rel_context -> bool list
+
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