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.

2 files changed, 17 insertions, 17 deletions

diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 6dfc32bf1a..8ea9a5f66a 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 2ef2896506..deb03f5160 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