Introducing contexts parameterized by the inner term type.

This allows the decoupling of the notions of context containing kernel
terms and context containing tactic-level terms.

5 files changed, 21 insertions, 21 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 0e4c6619b..3b5662a24 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -943,7 +943,7 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
   let tms = List.fold_right2 (fun par arg tomatch ->
     match EConstr.kind sigma par with
     | Rel i -> relocate_index_tomatch sigma (i+n) (destRel sigma arg) tomatch
-    | _ -> tomatch) (realargs@[cur]) (List.map EConstr.of_constr (Context.Rel.to_extended_list 0 sign))
+    | _ -> tomatch) (realargs@[cur]) (Context.Rel.to_extended_list EConstr.mkRel 0 sign)
        (lift_tomatch_stack n tms) in
   (* Pred is already dependent in the current term to match (if      *)
   (* (na<>Anonymous) and its realargs; we just need to adjust it to  *)
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 1adeb4db2..431d1ff16 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -63,7 +63,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, Context.Rel.to_extended_list 0 lnamespar) in
+  let indf = make_ind_family(pind, Context.Rel.to_extended_list mkRel 0 lnamespar) in
   let constrs = get_constructors env indf in
   let projs = get_projections env indf in
 
@@ -93,8 +93,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 Context.Rel.to_extended_vect 0 deparsign
-           else Context.Rel.to_extended_vect 1 arsign) in
+           if dep then Context.Rel.to_extended_vect mkRel 0 deparsign
+           else Context.Rel.to_extended_vect mkRel 1 arsign) in
       let p =
 	it_mkLambda_or_LetIn_name env'
 	  ((if dep then mkLambda_name env' else mkLambda)
@@ -168,7 +168,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), Context.Rel.to_extended_list 0 sign)|]
+                base [|applist (mkRel (i+1), Context.Rel.to_extended_list mkRel 0 sign)|]
             else
 	      base
       	| _ ->
@@ -244,7 +244,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), Context.Rel.to_extended_vect 0 hyps) in
+            and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect mkRel 0 hyps) in
             applist(lift i fk,realargs@[arg])
      	| _ ->
 	   let t' = whd_all env sigma (EConstr.of_constr p) 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 = Context.Rel.to_extended_list (nrec+nbconstruct) lnamesparrec in
+	    let args = Context.Rel.to_extended_list mkRel (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' = Context.Rel.to_extended_list (dect+nrec) lnamesparrec in
-	    let args'' = Context.Rel.to_extended_list ndepar lnonparrec in
+	    let args' = Context.Rel.to_extended_list mkRel (dect+nrec) lnamesparrec in
+	    let args'' = Context.Rel.to_extended_list mkRel 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, Context.Rel.to_extended_vect ndepar lnonparrec))
+		(fun f -> appvect (f, Context.Rel.to_extended_vect mkRel ndepar lnonparrec))
 		fi
 	      in
 		Array.map3
@@ -366,9 +366,9 @@ let mis_make_indrec env sigma listdepkind mib u =
 	    let deparsign' = LocalAssum (Anonymous,depind')::arsign' in
 
 	    let pargs =
-	      let nrpar = Context.Rel.to_extended_list (2*ndepar) lnonparrec
-	      and nrar = if dep then Context.Rel.to_extended_list 0 deparsign'
-		else Context.Rel.to_extended_list 1 arsign'
+	      let nrpar = Context.Rel.to_extended_list mkRel (2*ndepar) lnonparrec
+	      and nrar = if dep then Context.Rel.to_extended_list mkRel 0 deparsign'
+		else Context.Rel.to_extended_list mkRel 1 arsign'
 	      in nrpar@nrar
 
 	    in
@@ -396,8 +396,8 @@ let mis_make_indrec env sigma listdepkind mib u =
 
 	    let typtyi =
 	      let concl =
-		let pargs = if dep then Context.Rel.to_extended_vect 0 deparsign
-		  else Context.Rel.to_extended_vect 1 arsign
+		let pargs = if dep then Context.Rel.to_extended_vect mkRel 0 deparsign
+		  else Context.Rel.to_extended_vect mkRel 1 arsign
 		in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
 	      in it_mkProd_or_LetIn_name env
 		concl
@@ -424,7 +424,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 = Context.Rel.to_extended_list (nrec+i+j) lnamesparrec in
+	      let vargs = Context.Rel.to_extended_list mkRel (nrec+i+j) lnamesparrec in
 	      let cs = get_constructor ((indi,u),mibi,mipi,vargs) (j+1) in
 	      let p_0 =
 		type_rec_branch
@@ -438,7 +438,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), Context.Rel.to_extended_list i lnamesparrec) in
+	  let indf = make_ind_family ((indi,u), Context.Rel.to_extended_list mkRel 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/inductiveops.ml b/pretyping/inductiveops.ml
index 1dcd6399e..c00ceb02e 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -411,14 +411,14 @@ let build_dependent_constructor cs =
   applist
     (mkConstructU cs.cs_cstr,
      (List.map (lift cs.cs_nargs) cs.cs_params)
-      @(Context.Rel.to_extended_list 0 cs.cs_args))
+      @(Context.Rel.to_extended_list mkRel 0 cs.cs_args))
 
 let build_dependent_inductive env ((ind, params) as indf) =
   let arsign,_ = get_arity env indf in
   let nrealargs = List.length arsign in
   applist
     (mkIndU ind,
-     (List.map (lift nrealargs) params)@(Context.Rel.to_extended_list 0 arsign))
+     (List.map (lift nrealargs) params)@(Context.Rel.to_extended_list mkRel 0 arsign))
 
 (* builds the arity of an elimination predicate in sort [s] *)
 
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 9da7005e0..50ae66eb0 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -289,7 +289,7 @@ let build_subclasses ~check env sigma glob pri =
       | None -> []
       | Some (rels, ((tc,u), args)) ->
 	let instapp = 
-	  Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect 0 rels)))
+	  Reductionops.whd_beta sigma (EConstr.of_constr (appvectc c (Context.Rel.to_extended_vect mkRel 0 rels)))
 	in
 	let instapp = EConstr.Unsafe.to_constr instapp in
 	let projargs = Array.of_list (args @ [instapp]) in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1dc3ccdc0..04cc4253e 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1634,7 +1634,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
     | AllOccurrences, InHyp as occ ->
         let occ = if likefirst then LikeFirst else AtOccs occ in
         let newdecl = replace_term_occ_decl_modulo sigma occ test mkvarid d in
-        if Context.Named.Declaration.equal d newdecl
+        if Context.Named.Declaration.equal Constr.equal d newdecl
            && not (indirectly_dependent sigma c d depdecls)
         then
           if check_occs && not (in_every_hyp occs)