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.

1 files changed, 14 insertions, 0 deletions

diff --git a/kernel/context.ml b/kernel/context.ml
index 796f06d37..5923048fa 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