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.

13 files changed, 53 insertions, 46 deletions

diff --git a/engine/termops.ml b/engine/termops.ml
index 63baec129..db0f1e4db 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -158,19 +158,6 @@ let rel_list n m =
   in
   reln [] 1
 
-(* Same as [rel_list] but takes a context as argument and skips let-ins *)
-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)
-
-
-
 let push_rel_assum (x,t) env = push_rel (x,None,t) env
 
 let push_rels_assum assums =
diff --git a/engine/termops.mli b/engine/termops.mli
index 94c485a26..87f74f743 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -37,13 +37,9 @@ val lookup_rel_id : Id.t -> rel_context -> int * constr option * types
 
 (** Functions that build argument lists matching a block of binders or a context.
     [rel_vect n m] builds [|Rel (n+m);...;Rel(n+1)|]
-    [extended_rel_vect n ctx] extends the [ctx] context of length [m]
-    with [n] elements.
 *)
 val rel_vect : int -> int -> constr array
 val rel_list : int -> int -> constr list
-val extended_rel_list : int -> rel_context -> constr list
-val extended_rel_vect : int -> rel_context -> constr array
 
 (** iterators/destructors on terms *)
 val mkProd_or_LetIn : rel_declaration -> types -> types
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
diff --git a/kernel/context.mli b/kernel/context.mli
index 5279aefb6..735467747 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 cefb5eca5..466d48715 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
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 6dfc32bf1..8ea9a5f66 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -61,7 +61,7 @@ let check_privacy_block mib =
 
 let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
   let lnamespar = Vars.subst_instance_context u mib.mind_params_ctxt in
-  let indf = make_ind_family(pind, Termops.extended_rel_list 0 lnamespar) in
+  let indf = make_ind_family(pind, Context.extended_rel_list 0 lnamespar) in
   let constrs = get_constructors env indf in
   let projs = get_projections env indf in
 
@@ -92,8 +92,8 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind =
       let pbody =
         appvect
           (mkRel (ndepar + nbprod),
-           if dep then Termops.extended_rel_vect 0 deparsign
-           else Termops.extended_rel_vect 1 arsign) in
+           if dep then Context.extended_rel_vect 0 deparsign
+           else Context.extended_rel_vect 1 arsign) in
       let p =
 	it_mkLambda_or_LetIn_name env'
 	  ((if dep then mkLambda_name env' else mkLambda)
@@ -165,7 +165,7 @@ let type_rec_branch is_rec dep env sigma (vargs,depPvect,decP) tyi cs recargs =
 	    let base = applist (lift i pk,realargs) in
             if depK then
 	      Reduction.beta_appvect
-                base [|applist (mkRel (i+1), Termops.extended_rel_list 0 sign)|]
+                base [|applist (mkRel (i+1), Context.extended_rel_list 0 sign)|]
             else
 	      base
       	| _ -> assert false
@@ -237,7 +237,7 @@ let make_rec_branch_arg env sigma (nparrec,fvect,decF) f cstr recargs =
 	    mkLetIn (n,b,t,prec (push_rel d env) (i+1) (d::hyps) c)
      	| Ind _ ->
             let realargs = List.skipn nparrec largs
-            and arg = appvect (mkRel (i+1), Termops.extended_rel_vect 0 hyps) in
+            and arg = appvect (mkRel (i+1), Context.extended_rel_vect 0 hyps) in
             applist(lift i fk,realargs@[arg])
      	| _ -> assert false
     in
@@ -323,7 +323,7 @@ let mis_make_indrec env sigma listdepkind mib u =
 
             (* arity in the context of the fixpoint, i.e.
                P1..P_nrec f1..f_nbconstruct *)
-	    let args = Termops.extended_rel_list (nrec+nbconstruct) lnamesparrec in
+	    let args = Context.extended_rel_list (nrec+nbconstruct) lnamesparrec in
 	    let indf = make_ind_family((indi,u),args) in
 
 	    let arsign,_ = get_arity env indf in
@@ -337,15 +337,15 @@ let mis_make_indrec env sigma listdepkind mib u =
 
             (* constructors in context of the Cases expr, i.e.
                P1..P_nrec f1..f_nbconstruct F_1..F_nrec a_1..a_nar x:I *)
-	    let args' = Termops.extended_rel_list (dect+nrec) lnamesparrec in
-	    let args'' = Termops.extended_rel_list ndepar lnonparrec in
+	    let args' = Context.extended_rel_list (dect+nrec) lnamesparrec in
+	    let args'' = Context.extended_rel_list ndepar lnonparrec in
             let indf' = make_ind_family((indi,u),args'@args'') in
 
 	    let branches =
 	      let constrs = get_constructors env indf' in
 	      let fi = Termops.rel_vect (dect-i-nctyi) nctyi in
 	      let vecfi = Array.map
-		(fun f -> appvect (f, Termops.extended_rel_vect ndepar lnonparrec))
+		(fun f -> appvect (f, Context.extended_rel_vect ndepar lnonparrec))
 		fi
 	      in
 		Array.map3
@@ -366,9 +366,9 @@ let mis_make_indrec env sigma listdepkind mib u =
 	    let deparsign' = (Anonymous,None,depind')::arsign' in
 
 	    let pargs =
-	      let nrpar = Termops.extended_rel_list (2*ndepar) lnonparrec
-	      and nrar = if dep then Termops.extended_rel_list 0 deparsign'
-		else Termops.extended_rel_list 1 arsign'
+	      let nrpar = Context.extended_rel_list (2*ndepar) lnonparrec
+	      and nrar = if dep then Context.extended_rel_list 0 deparsign'
+		else Context.extended_rel_list 1 arsign'
 	      in nrpar@nrar
 
 	    in
@@ -411,8 +411,8 @@ let mis_make_indrec env sigma listdepkind mib u =
 
 	    let typtyi =
 	      let concl =
-		let pargs = if dep then Termops.extended_rel_vect 0 deparsign
-		  else Termops.extended_rel_vect 1 arsign
+		let pargs = if dep then Context.extended_rel_vect 0 deparsign
+		  else Context.extended_rel_vect 1 arsign
 		in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
 	      in it_mkProd_or_LetIn_name env
 		concl
@@ -439,7 +439,7 @@ let mis_make_indrec env sigma listdepkind mib u =
 	    else
 	      let recarg = (dest_subterms recargsvec.(tyi)).(j) in
 	      let recarg = recargpar@recarg in
-	      let vargs = Termops.extended_rel_list (nrec+i+j) lnamesparrec in
+	      let vargs = Context.extended_rel_list (nrec+i+j) lnamesparrec in
 	      let cs = get_constructor ((indi,u),mibi,mipi,vargs) (j+1) in
 	      let p_0 =
 		type_rec_branch
@@ -453,7 +453,7 @@ let mis_make_indrec env sigma listdepkind mib u =
     in
     let rec put_arity env i = function
       | ((indi,u),_,_,dep,kinds)::rest ->
-	  let indf = make_ind_family ((indi,u), Termops.extended_rel_list i lnamesparrec) in
+	  let indf = make_ind_family ((indi,u), Context.extended_rel_list i lnamesparrec) in
 	  let s = 
 	    Evarutil.evd_comb1 (Evd.fresh_sort_in_family ~rigid:Evd.univ_flexible_alg env) 
 	      evdref kinds 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2ef289650..deb03f516 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -287,7 +287,7 @@ let build_subclasses ~check env sigma glob pri =
       | None -> []
       | Some (rels, ((tc,u), args)) ->
 	let instapp = 
-	  Reductionops.whd_beta sigma (appvectc c (Termops.extended_rel_vect 0 rels)) 
+	  Reductionops.whd_beta sigma (appvectc c (Context.extended_rel_vect 0 rels))
 	in
 	let projargs = Array.of_list (args @ [instapp]) in
 	let projs = List.map_filter 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 1d275c1aa..d6f847cc7 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -65,6 +65,7 @@ let get_new_id locals id =
 
 (** Inductive declarations *)
 
+open Context
 open Termops
 open Reduction
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e80f5a64c..1ba14e7d4 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -13,6 +13,7 @@ open Names
 open Nameops
 open Term
 open Vars
+open Context
 open Termops
 open Environ
 open Reductionops
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ff1ed4030..0f907b0ef 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -315,7 +315,7 @@ let project_hint pri l2r r =
     | _ -> assert false in
   let p =
     if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
-  let c = Reductionops.whd_beta Evd.empty (mkApp (c,Termops.extended_rel_vect 0 sign)) in
+  let c = Reductionops.whd_beta Evd.empty (mkApp (c,Context.extended_rel_vect 0 sign)) in
   let c = it_mkLambda_or_LetIn
     (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
   let id =
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index e99b609b6..98686fb1b 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -15,6 +15,7 @@ open Util
 open Pp
 open Term
 open Vars
+open Context
 open Termops
 open Declarations
 open Names
diff --git a/toplevel/class.ml b/toplevel/class.ml
index da6624032..22baa5e61 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -12,6 +12,7 @@ open Pp
 open Names
 open Term
 open Vars
+open Context
 open Termops
 open Entries
 open Environ
diff --git a/toplevel/record.ml b/toplevel/record.ml
index dc2c9264b..3a75004b0 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -244,8 +244,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
   let ctx = Univ.instantiate_univ_context mib.mind_universes in
   let indu = indsp, u in
   let r = mkIndU (indsp,u) in
-  let rp = applist (r, Termops.extended_rel_list 0 paramdecls) in
-  let paramargs = Termops.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
+  let rp = applist (r, Context.extended_rel_list 0 paramdecls) in
+  let paramargs = Context.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
   let x = Name binder_name in
   let fields = instantiate_possibly_recursive_type indu paramdecls fields in
   let lifted_fields = Termops.lift_rel_context 1 fields in
@@ -353,7 +353,7 @@ open Typeclasses
 let declare_structure finite poly ctx id idbuild paramimpls params arity template 
     fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
   let nparams = List.length params and nfields = List.length fields in
-  let args = Termops.extended_rel_list nfields params in
+  let args = Context.extended_rel_list nfields params in
   let ind = applist (mkRel (1+nparams+nfields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
   let binder_name =