merge

23 files changed, 113 insertions, 133 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index b894cb8ea4..adcaa64412 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -13,7 +13,6 @@ open Names
 open Nameops
 open Term
 open Vars
-open Context
 open Termops
 open Namegen
 open Declarations
@@ -131,7 +130,7 @@ type tomatch_status =
   | Pushed of (bool*((constr * tomatch_type) * int list * Name.t))
   | Alias of (bool*(Name.t * constr * (constr * types)))
   | NonDepAlias
-  | Abstract of int * rel_declaration
+  | Abstract of int * Context.Rel.Declaration.t
 
 type tomatch_stack = tomatch_status list
 
@@ -602,7 +601,7 @@ let relocate_index_tomatch n1 n2 =
       NonDepAlias :: genrec depth rest
   | Abstract (i,d) :: rest ->
       let i = relocate_rel n1 n2 depth i in
-      Abstract (i,map_rel_declaration (relocate_index n1 n2 depth) d)
+      Abstract (i, Context.Rel.Declaration.map (relocate_index n1 n2 depth) d)
       :: genrec (depth+1) rest in
   genrec 0
 
@@ -635,7 +634,7 @@ let replace_tomatch n c =
   | NonDepAlias  :: rest ->
       NonDepAlias :: replrec depth rest
   | Abstract (i,d) :: rest ->
-      Abstract (i,map_rel_declaration (replace_term n c depth) d)
+      Abstract (i, Context.Rel.Declaration.map (replace_term n c depth) d)
       :: replrec (depth+1) rest in
   replrec 0
 
@@ -660,7 +659,7 @@ let rec liftn_tomatch_stack n depth = function
       NonDepAlias :: liftn_tomatch_stack n depth rest
   | Abstract (i,d)::rest ->
       let i = if i<depth then i else i+n in
-      Abstract (i,map_rel_declaration (liftn n depth) d)
+      Abstract (i, Context.Rel.Declaration.map (liftn n depth) d)
       ::(liftn_tomatch_stack n (depth+1) rest)
 
 let lift_tomatch_stack n = liftn_tomatch_stack n 1
@@ -921,7 +920,7 @@ let abstract_predicate env sigma indf cur realargs (names,na) tms ccl =
   let tms = List.fold_right2 (fun par arg tomatch ->
     match kind_of_term par with
     | Rel i -> relocate_index_tomatch (i+n) (destRel arg) tomatch
-    | _ -> tomatch) (realargs@[cur]) (extended_rel_list 0 sign)
+    | _ -> tomatch) (realargs@[cur]) (Context.Rel.to_extended_list 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  *)
@@ -1118,7 +1117,7 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs =
   let rec aux k brs tomatch pred tocheck deps = match deps, tomatch with
   | [], _ -> brs,tomatch,pred,[]
   | n::deps, Abstract (i,d) :: tomatch ->
-      let d = map_rel_declaration (nf_evar evd) d in
+      let d = Context.Rel.Declaration.map (nf_evar evd) d in
       let is_d = match d with (_, None, _) -> false | _ -> true in
       if is_d || List.exists (fun c -> dependent_decl (lift k c) d) tocheck
                  && Array.exists (is_dependent_branch k) brs then
@@ -1187,7 +1186,7 @@ let group_equations pb ind current cstrs mat =
 let rec generalize_problem names pb = function
   | [] -> pb, []
   | i::l ->
-      let (na,b,t as d) = map_rel_declaration (lift i) (Environ.lookup_rel i pb.env) in
+      let (na,b,t as d) = Context.Rel.Declaration.map (lift i) (Environ.lookup_rel i pb.env) in
       let pb',deps = generalize_problem names pb l in
       begin match (na, b) with
       | Anonymous, Some _ -> pb', deps
@@ -1230,7 +1229,7 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn
   (* We adjust the terms to match in the context they will be once the *)
   (* context [x1:T1,..,xn:Tn] will have been pushed on the current env *)
   let typs' =
-    List.map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 typs in
+    List.map_i (fun i d -> (mkRel i, Context.Rel.Declaration.map (lift i) d)) 1 typs in
 
   let extenv = push_rel_context typs pb.env in
 
@@ -1560,8 +1559,8 @@ let matx_of_eqns env eqns =
 *)
 
 let adjust_to_extended_env_and_remove_deps env extenv subst t =
-  let n = rel_context_length (rel_context env) in
-  let n' = rel_context_length (rel_context extenv) in
+  let n = Context.Rel.length (rel_context env) in
+  let n' = Context.Rel.length (rel_context extenv) in
   (* We first remove the bindings that are dependently typed (they are
      difficult to manage and it is not sure these are so useful in practice);
      Notes:
@@ -1673,8 +1672,8 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t =
     | None ->
 	(* This is the situation we are building a return predicate and
            we are in an impossible branch *)
-	let n = rel_context_length (rel_context env) in
-	let n' = rel_context_length (rel_context tycon_env) in
+	let n = Context.Rel.length (rel_context env) in
+	let n' = Context.Rel.length (rel_context tycon_env) in
 	let impossible_case_type, u =
 	  e_new_type_evar (reset_context env) evdref univ_flexible_alg ~src:(loc,Evar_kinds.ImpossibleCase) in
 	(lift (n'-n) impossible_case_type, mkSort u)
@@ -1744,7 +1743,7 @@ let build_inversion_problem loc env sigma tms t =
   let n = List.length sign in
 
   let decls =
-    List.map_i (fun i d -> (mkRel i,map_rel_declaration (lift i) d)) 1 sign in
+    List.map_i (fun i d -> (mkRel i, Context.Rel.Declaration.map (lift i) d)) 1 sign in
 
   let pb_env = push_rel_context sign env in
   let decls =
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index c599766ab7..4ec71956b4 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Evd
 open Environ
 open Inductiveops
@@ -45,11 +44,11 @@ val compile_cases :
 val constr_of_pat : 
            Environ.env ->
            Evd.evar_map ref ->
-           rel_declaration list ->
+           Context.Rel.Declaration.t list ->
            Glob_term.cases_pattern ->
            Names.Id.t list ->
            Glob_term.cases_pattern *
-           (rel_declaration list * Term.constr *
+           (Context.Rel.Declaration.t list * Term.constr *
             (Term.types * Term.constr list) * Glob_term.cases_pattern) *
            Names.Id.t list
 
@@ -83,7 +82,7 @@ type tomatch_status =
   | Pushed of (bool*((constr * tomatch_type) * int list * Name.t))
   | Alias of (bool * (Name.t * constr * (constr * types)))
   | NonDepAlias
-  | Abstract of int * rel_declaration
+  | Abstract of int * Context.Rel.Declaration.t
 
 type tomatch_stack = tomatch_status list
 
@@ -117,7 +116,7 @@ val prepare_predicate :            Loc.t ->
            Environ.env ->
            Evd.evar_map ->
            (Term.types * tomatch_type) list ->
-           Context.rel_context list ->
+           Context.Rel.t list ->
            Constr.constr option ->
            'a option -> (Evd.evar_map * Names.name list * Term.constr) list
 
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 5e99521a12..0b0bd8304e 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -17,7 +17,6 @@ open Termops
 open Reductionops
 open Term
 open Vars
-open Context
 open Pattern
 open Patternops
 open Misctypes
@@ -269,8 +268,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
       | PIf (a1,b1,b1'), Case (ci,_,a2,[|b2;b2'|]) ->
 	  let ctx_b2,b2 = decompose_lam_n_decls ci.ci_cstr_ndecls.(0) b2 in
 	  let ctx_b2',b2' = decompose_lam_n_decls ci.ci_cstr_ndecls.(1) b2' in
-	  let n = rel_context_length ctx_b2 in
-          let n' = rel_context_length ctx_b2' in
+	  let n = Context.Rel.length ctx_b2 in
+          let n' = Context.Rel.length ctx_b2' in
 	  if noccur_between 1 n b2 && noccur_between 1 n' b2' then
             let f l (na,_,t) = (Anonymous,na,t)::l in
 	    let ctx_br = List.fold_left f ctx ctx_b2 in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index dab82fa22b..4ca066feb0 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -12,7 +12,6 @@ open Util
 open Names
 open Term
 open Vars
-open Context
 open Inductiveops
 open Environ
 open Glob_term
@@ -199,7 +198,7 @@ let computable p k =
        engendrera un prédicat non dépendant) *)
 
   let sign,ccl = decompose_lam_assum p in
-  Int.equal (rel_context_length sign) (k + 1)
+  Int.equal (Context.Rel.length sign) (k + 1)
   &&
   noccur_between 1 (k+1) ccl
 
@@ -315,7 +314,7 @@ let is_nondep_branch c l =
   try
     (* FIXME: do better using tags from l *)
     let sign,ccl = decompose_lam_n_decls (List.length l) c in
-    noccur_between 1 (rel_context_length sign) ccl
+    noccur_between 1 (Context.Rel.length sign) ccl
   with e when Errors.noncritical e -> (* Not eta-expanded or not reduced *)
     false
 
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index eb158686aa..f8f8093c0f 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Environ
 open Glob_term
 open Termops
@@ -46,7 +45,7 @@ val detype_case :
 val detype_sort : evar_map -> sorts -> glob_sort
 
 val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> 
-  evar_map -> rel_context -> glob_decl list
+  evar_map -> Context.Rel.t -> glob_decl list
 
 val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr
 
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 69e8e9d988..af2877d34f 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -11,7 +11,6 @@ open Errors
 open Names
 open Term
 open Vars
-open Context
 open Environ
 open Termops
 open Evd
@@ -501,7 +500,7 @@ let solve_pattern_eqn env l c =
     match kind_of_term a with
       (* Rem: if [a] links to a let-in, do as if it were an assumption *)
       | Rel n ->
-          let d = map_rel_declaration (lift n) (lookup_rel n env) in
+          let d = Context.Rel.Declaration.map (lift n) (lookup_rel n env) in
           mkLambda_or_LetIn d c'
       | Var id ->
           let d = lookup_named id env in mkNamedLambda_or_LetIn d c'
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 3c3afac54e..f001d6e3e9 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -12,7 +12,6 @@ open Pp
 open Names
 open Term
 open Vars
-open Context
 open Termops
 open Namegen
 open Pre_env
@@ -78,12 +77,12 @@ let tj_nf_evar sigma {utj_val=v;utj_type=t} =
 
 let env_nf_evar sigma env =
   process_rel_context
-    (fun d e -> push_rel (map_rel_declaration (nf_evar sigma) d) e) env
+    (fun d e -> push_rel (Context.Rel.Declaration.map (nf_evar sigma) d) e) env
 
 let env_nf_betaiotaevar sigma env =
   process_rel_context
     (fun d e ->
-      push_rel (map_rel_declaration (Reductionops.nf_betaiota sigma) d) e) env
+      push_rel (Context.Rel.Declaration.map (Reductionops.nf_betaiota sigma) d) e) env
 
 let nf_evars_universes evm =
   Universes.nf_evars_and_universes_opt_subst (Reductionops.safe_evar_value evm) 
@@ -106,10 +105,10 @@ let nf_evar_map_universes evm =
 	Evd.raw_map (fun _ -> map_evar_info f) evm, f
 
 let nf_named_context_evar sigma ctx =
-  Context.map_named_context (nf_evar sigma) ctx
+  Context.Named.map (nf_evar sigma) ctx
 
 let nf_rel_context_evar sigma ctx =
-  Context.map_rel_context (nf_evar sigma) ctx
+  Context.Rel.map (nf_evar sigma) ctx
 
 let nf_env_evar sigma env =
   let nc' = nf_named_context_evar sigma (Environ.named_context env) in
@@ -303,7 +302,7 @@ let push_rel_context_to_named_context env typ =
   (* with vars of the rel context *)
   (* We do keep the instances corresponding to local definition (see above) *)
   let (subst, vsubst, _, env) =
-    Context.fold_rel_context
+    Context.Rel.fold_outside
       (fun (na,c,t) (subst, vsubst, avoid, env) ->
         let id =
           (* ppedrot: we want to infer nicer names for the refine tactic, but
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 96648bb111..867917c9cf 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Evd
 open Environ
 
@@ -129,7 +128,7 @@ val gather_dependent_evars : evar_map -> evar list -> (Evar.Set.t option) Evar.M
     [nf_evar]. *)
 
 val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t
-val undefined_evars_of_named_context : evar_map -> named_context -> Evar.Set.t
+val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t
 val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t
 
 (** [occur_evar_upto sigma k c] returns [true] if [k] appears in
@@ -170,8 +169,8 @@ val jv_nf_evar :
 val tj_nf_evar :
    evar_map -> unsafe_type_judgment -> unsafe_type_judgment
 
-val nf_named_context_evar : evar_map -> named_context -> named_context
-val nf_rel_context_evar : evar_map -> rel_context -> rel_context
+val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t
+val nf_rel_context_evar : evar_map -> Context.Rel.t -> Context.Rel.t
 val nf_env_evar : evar_map -> env -> env
 
 val nf_evar_info : evar_map -> evar_info -> evar_info
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 47d9654e57..1366c34ce2 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Locus
-open Context
 open Term
 open Evd
 open Pretype_errors
@@ -50,7 +49,7 @@ val replace_term_occ_modulo : occurrences or_like_first ->
 val replace_term_occ_decl_modulo :
   (occurrences * hyp_location_flag) or_like_first ->
   'a testing_function -> (unit -> constr) ->
-  named_declaration -> named_declaration
+  Context.Named.Declaration.t -> Context.Named.Declaration.t
 
 (** [subst_closed_term_occ occl c d] replaces occurrences of
     closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC),
@@ -62,7 +61,7 @@ val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first ->
     closed [c] at positions [occl] by [Rel 1] in [decl]. *)
 val subst_closed_term_occ_decl : env -> evar_map ->
   (occurrences * hyp_location_flag) or_like_first ->
-  constr -> named_declaration -> named_declaration * evar_map
+  constr -> Context.Named.Declaration.t -> Context.Named.Declaration.t * evar_map
 
 (** Miscellaneous *)
 val error_invalid_occurrence : int list -> 'a
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 3f21842e39..40175dac91 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -19,7 +19,6 @@ open Globnames
 open Nameops
 open Term
 open Vars
-open Context
 open Namegen
 open Declarations
 open Declareops
@@ -61,7 +60,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.extended_rel_list 0 lnamespar) in
+  let indf = make_ind_family(pind, Context.Rel.to_extended_list 0 lnamespar) in
   let constrs = get_constructors env indf in
   let projs = get_projections env indf in
 
@@ -92,8 +91,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.extended_rel_vect 0 deparsign
-           else Context.extended_rel_vect 1 arsign) in
+           if dep then Context.Rel.to_extended_vect 0 deparsign
+           else Context.Rel.to_extended_vect 1 arsign) in
       let p =
 	it_mkLambda_or_LetIn_name env'
 	  ((if dep then mkLambda_name env' else mkLambda)
@@ -165,7 +164,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.extended_rel_list 0 sign)|]
+                base [|applist (mkRel (i+1), Context.Rel.to_extended_list 0 sign)|]
             else
 	      base
       	| _ -> assert false
@@ -237,7 +236,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.extended_rel_vect 0 hyps) in
+            and arg = appvect (mkRel (i+1), Context.Rel.to_extended_vect 0 hyps) in
             applist(lift i fk,realargs@[arg])
      	| _ -> assert false
     in
@@ -312,29 +311,29 @@ 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.extended_rel_list (nrec+nbconstruct) lnamesparrec in
+	    let args = Context.Rel.to_extended_list (nrec+nbconstruct) lnamesparrec in
 	    let indf = make_ind_family((indi,u),args) in
 
 	    let arsign,_ = get_arity env indf in
 	    let depind = build_dependent_inductive env indf in
 	    let deparsign = (Anonymous,None,depind)::arsign in
 
-	    let nonrecpar = rel_context_length lnonparrec in
-	    let larsign = rel_context_length deparsign in
+	    let nonrecpar = Context.Rel.length lnonparrec in
+	    let larsign = Context.Rel.length deparsign in
 	    let ndepar = larsign - nonrecpar in
 	    let dect = larsign+nrec+nbconstruct in
 
             (* 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.extended_rel_list (dect+nrec) lnamesparrec in
-	    let args'' = Context.extended_rel_list ndepar lnonparrec in
+	    let args' = Context.Rel.to_extended_list (dect+nrec) lnamesparrec in
+	    let args'' = Context.Rel.to_extended_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, Context.extended_rel_vect ndepar lnonparrec))
+		(fun f -> appvect (f, Context.Rel.to_extended_vect ndepar lnonparrec))
 		fi
 	      in
 		Array.map3
@@ -355,9 +354,9 @@ let mis_make_indrec env sigma listdepkind mib u =
 	    let deparsign' = (Anonymous,None,depind')::arsign' in
 
 	    let pargs =
-	      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'
+	      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'
 	      in nrpar@nrar
 
 	    in
@@ -400,14 +399,14 @@ let mis_make_indrec env sigma listdepkind mib u =
 
 	    let typtyi =
 	      let concl =
-		let pargs = if dep then Context.extended_rel_vect 0 deparsign
-		  else Context.extended_rel_vect 1 arsign
+		let pargs = if dep then Context.Rel.to_extended_vect 0 deparsign
+		  else Context.Rel.to_extended_vect 1 arsign
 		in appvect (mkRel (nbconstruct+ndepar+nonrecpar+j),pargs)
 	      in it_mkProd_or_LetIn_name env
 		concl
 		deparsign
 	    in
-	      mrec (i+nctyi) (rel_context_nhyps arsign ::ln) (typtyi::ltyp)
+	      mrec (i+nctyi) (Context.Rel.nhyps arsign ::ln) (typtyi::ltyp)
                 (deftyi::ldef) rest
         | [] ->
 	    let fixn = Array.of_list (List.rev ln) in
@@ -428,7 +427,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.extended_rel_list (nrec+i+j) lnamesparrec in
+	      let vargs = Context.Rel.to_extended_list (nrec+i+j) lnamesparrec in
 	      let cs = get_constructor ((indi,u),mibi,mipi,vargs) (j+1) in
 	      let p_0 =
 		type_rec_branch
@@ -442,7 +441,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.extended_rel_list i lnamesparrec) in
+	  let indf = make_ind_family ((indi,u), Context.Rel.to_extended_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/inductiveops.ml b/pretyping/inductiveops.ml
index f429c51eb8..1e3ff0fa2d 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -12,7 +12,6 @@ open Names
 open Univ
 open Term
 open Vars
-open Context
 open Termops
 open Declarations
 open Declareops
@@ -142,12 +141,12 @@ let constructor_nallargs_env env ((kn,i),j) =
 
 let constructor_nalldecls (indsp,j) = (* TOCHANGE en decls *)
   let (mib,mip) = Global.lookup_inductive indsp in
-  mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt)
+  mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt)
 
 let constructor_nalldecls_env env ((kn,i),j) = (* TOCHANGE en decls *)
   let mib = Environ.lookup_mind kn env in
   let mip = mib.mind_packets.(i) in
-  mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt)
+  mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt)
 
 (* Arity of constructors excluding params, excluding local defs *)
 
@@ -213,21 +212,21 @@ let inductive_nparams_env env ind =
 
 let inductive_nparamdecls ind =
   let (mib,mip) = Global.lookup_inductive ind in
-  rel_context_length mib.mind_params_ctxt
+  Context.Rel.length mib.mind_params_ctxt
 
 let inductive_nparamdecls_env env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  rel_context_length mib.mind_params_ctxt
+  Context.Rel.length mib.mind_params_ctxt
 
 (* Full length of arity (with local defs) *)
 
 let inductive_nalldecls ind =
   let (mib,mip) = Global.lookup_inductive ind in
-  rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls
+  Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls
 
 let inductive_nalldecls_env env ind =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
-  rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls
+  Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls
 
 (* Others *)
 
@@ -249,13 +248,13 @@ let inductive_alldecls_env env (ind,u) =
 
 let constructor_has_local_defs (indsp,j) =
   let (mib,mip) = Global.lookup_inductive indsp in
-  let l1 = mip.mind_consnrealdecls.(j-1) + rel_context_length (mib.mind_params_ctxt) in
+  let l1 = mip.mind_consnrealdecls.(j-1) + Context.Rel.length (mib.mind_params_ctxt) in
   let l2 = recarg_length mip.mind_recargs j + mib.mind_nparams in
   not (Int.equal l1 l2)
 
 let inductive_has_local_defs ind =
   let (mib,mip) = Global.lookup_inductive ind in
-  let l1 = rel_context_length (mib.mind_params_ctxt) + mip.mind_nrealdecls in
+  let l1 = Context.Rel.length (mib.mind_params_ctxt) + mip.mind_nrealdecls in
   let l2 = mib.mind_nparams + mip.mind_nrealargs in
   not (Int.equal l1 l2)
 
@@ -273,11 +272,11 @@ let projection_nparams p = projection_nparams_env (Global.env ()) p
 let make_case_info env ind style =
   let (mib,mip) = Inductive.lookup_mind_specif env ind in
   let ind_tags =
-    rel_context_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in
+    Context.Rel.to_tags (List.firstn mip.mind_nrealdecls mip.mind_arity_ctxt) in
   let cstr_tags =
     Array.map2 (fun c n ->
       let d,_ = decompose_prod_assum c in
-      rel_context_tags (List.firstn n d))
+      Context.Rel.to_tags (List.firstn n d))
       mip.mind_nf_lc mip.mind_consnrealdecls in
   let print_info = { ind_tags; cstr_tags; style } in
   { ci_ind     = ind;
@@ -292,7 +291,7 @@ type constructor_summary = {
   cs_cstr : pconstructor;
   cs_params : constr list;
   cs_nargs : int;
-  cs_args : rel_context;
+  cs_args : Context.Rel.t;
   cs_concl_realargs : constr array
 }
 
@@ -306,10 +305,10 @@ let lift_constructor n cs = {
 
 (* Accept either all parameters or only recursively uniform ones *)
 let instantiate_params t params sign =
-  let nnonrecpar = rel_context_nhyps sign - List.length params in
+  let nnonrecpar = Context.Rel.nhyps sign - List.length params in
   (* Adjust the signature if recursively non-uniform parameters are not here *)
   let _,sign = context_chop nnonrecpar sign in
-  let _,t = decompose_prod_n_assum (rel_context_length sign) t in
+  let _,t = decompose_prod_n_assum (Context.Rel.length sign) t in
   let subst = subst_of_rel_context_instance sign params in
   substl subst t
 
@@ -323,7 +322,7 @@ let get_constructor ((ind,u as indu),mib,mip,params) j =
   let vargs = List.skipn (List.length params) allargs in
   { cs_cstr = (ith_constructor_of_inductive ind j,u);
     cs_params = params;
-    cs_nargs = rel_context_length args;
+    cs_nargs = Context.Rel.length args;
     cs_args = args;
     cs_concl_realargs = Array.of_list vargs }
 
@@ -374,14 +373,14 @@ let build_dependent_constructor cs =
   applist
     (mkConstructU cs.cs_cstr,
      (List.map (lift cs.cs_nargs) cs.cs_params)
-      @(extended_rel_list 0 cs.cs_args))
+      @(Context.Rel.to_extended_list 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)@(extended_rel_list 0 arsign))
+     (List.map (lift nrealargs) params)@(Context.Rel.to_extended_list 0 arsign))
 
 (* builds the arity of an elimination predicate in sort [s] *)
 
@@ -506,7 +505,7 @@ let set_pattern_names env ind brv =
   let arities =
     Array.map
       (fun c ->
-        rel_context_length ((prod_assum c)) -
+        Context.Rel.length ((prod_assum c)) -
         mib.mind_nparams)
       mip.mind_nf_lc in
   Array.map2 (set_names env) arities brv
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 9036f521ec..42a00a7e22 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Declarations
 open Environ
 open Evd
@@ -92,12 +91,12 @@ val inductive_nparamdecls : inductive -> int
 val inductive_nparamdecls_env : env -> inductive -> int
 
 (** @return params context *)
-val inductive_paramdecls : pinductive -> rel_context
-val inductive_paramdecls_env : env -> pinductive -> rel_context
+val inductive_paramdecls : pinductive -> Context.Rel.t
+val inductive_paramdecls_env : env -> pinductive -> Context.Rel.t
 
 (** @return full arity context, hence with letin *)
-val inductive_alldecls : pinductive -> rel_context
-val inductive_alldecls_env : env -> pinductive -> rel_context
+val inductive_alldecls : pinductive -> Context.Rel.t
+val inductive_alldecls_env : env -> pinductive -> Context.Rel.t
 
 (** {7 Extract information from a constructor name} *)
 
@@ -133,9 +132,9 @@ val type_of_projection_knowing_arg : env -> evar_map -> Projection.t ->
 
 type constructor_summary = {
   cs_cstr : pconstructor;    (* internal name of the constructor plus universes *)
-  cs_params : constr list;  (* parameters of the constructor in current ctx *)
-  cs_nargs : int;           (* length of arguments signature (letin included) *)
-  cs_args : rel_context;    (* signature of the arguments (letin included) *)
+  cs_params : constr list;   (* parameters of the constructor in current ctx *)
+  cs_nargs : int;            (* length of arguments signature (letin included) *)
+  cs_args : Context.Rel.t;   (* signature of the arguments (letin included) *)
   cs_concl_realargs : constr array; (* actual realargs in the concl of cstr *)
 }
 val lift_constructor : int -> constructor_summary -> constructor_summary
@@ -148,11 +147,11 @@ val get_projections  : env -> inductive_family -> constant array option
 (** [get_arity] returns the arity of the inductive family instantiated
     with the parameters; if recursively non-uniform parameters are not
     part of the inductive family, they appears in the arity *)
-val get_arity        : env -> inductive_family -> rel_context * sorts_family
+val get_arity        : env -> inductive_family -> Context.Rel.t * sorts_family
 
 val build_dependent_constructor : constructor_summary -> constr
 val build_dependent_inductive   : env -> inductive_family -> constr
-val make_arity_signature : env -> bool -> inductive_family -> rel_context
+val make_arity_signature : env -> bool -> inductive_family -> Context.Rel.t
 val make_arity : env -> bool -> inductive_family -> sorts -> types
 val build_branch_type : env -> bool -> constr -> constructor_summary -> types
 
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 7d54969171..84beaa9e3c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -28,7 +28,6 @@ open Names
 open Evd
 open Term
 open Vars
-open Context
 open Termops
 open Reductionops
 open Environ
@@ -311,7 +310,7 @@ let ltac_interp_name_env k0 lvar env =
      specification of pretype which accepts to start with a non empty
      rel_context) *)
   (* tail is the part of the env enriched by pretyping *)
-  let n = rel_context_length (rel_context env) - k0 in
+  let n = Context.Rel.length (rel_context env) - k0 in
   let ctxt,_ = List.chop n (rel_context env) in
   let env = pop_rel_context n env in
   let ctxt = List.map (fun (na,c,t) -> ltac_interp_name lvar na,c,t) ctxt in
@@ -515,14 +514,14 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
         let ty' = pretype_type empty_valcon env evdref lvar ty in
         let dcl = (na,None,ty'.utj_val) in
         let dcl' = (ltac_interp_name lvar na,None,ty'.utj_val) in
-	  type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl
+	  type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl
       | (na,bk,Some bd,ty)::bl ->
         let ty' = pretype_type empty_valcon env evdref lvar ty in
         let bd' = pretype (mk_tycon ty'.utj_val) env evdref lvar bd in
         let dcl = (na,Some bd'.uj_val,ty'.utj_val) in
         let dcl' = (ltac_interp_name lvar na,Some bd'.uj_val,ty'.utj_val) in
-	  type_bl (push_rel dcl env) (add_rel_decl dcl' ctxt) bl in
-    let ctxtv = Array.map (type_bl env empty_rel_context) bl in
+	  type_bl (push_rel dcl env) (Context.Rel.add dcl' ctxt) bl in
+    let ctxtv = Array.map (type_bl env Context.Rel.empty) bl in
     let larj =
       Array.map2
         (fun e ar ->
@@ -549,7 +548,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
              (* we lift nbfix times the type in tycon, because of
 	      * the nbfix variables pushed to newenv *)
           let (ctxt,ty) =
-	    decompose_prod_n_assum (rel_context_length ctxt)
+	    decompose_prod_n_assum (Context.Rel.length ctxt)
               (lift nbfix ftys.(i)) in
           let nenv = push_rel_context ctxt newenv in
           let j = pretype (mk_tycon ty) nenv evdref lvar def in
@@ -870,7 +869,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_
       let pred = nf_evar !evdref pred in
       let p = nf_evar !evdref p in
       let f cs b =
-	let n = rel_context_length cs.cs_args in
+	let n = Context.Rel.length cs.cs_args in
 	let pi = lift n pred in (* liftn n 2 pred ? *)
 	let pi = beta_applist (pi, [build_dependent_constructor cs]) in
 	let csgn =
@@ -1003,7 +1002,7 @@ and pretype_type k0 resolve_tc valcon env evdref lvar = function
 
 let ise_pretype_gen flags env sigma lvar kind c =
   let evdref = ref sigma in
-  let k0 = rel_context_length (rel_context env) in
+  let k0 = Context.Rel.length (rel_context env) in
   let c' = match kind with
     | WithoutTypeConstraint ->
         (pretype k0 flags.use_typeclasses empty_tycon env evdref lvar c).uj_val
@@ -1045,7 +1044,7 @@ let on_judgment f j =
 
 let understand_judgment env sigma c =
   let evdref = ref sigma in
-  let k0 = rel_context_length (rel_context env) in
+  let k0 = Context.Rel.length (rel_context env) in
   let j = pretype k0 true empty_tycon env evdref empty_lvar c in
   let j = on_judgment (fun c ->
     let evd, c = process_inference_flags all_and_fail_flags env sigma (!evdref,c) in 
@@ -1053,7 +1052,7 @@ let understand_judgment env sigma c =
   in j, Evd.evar_universe_context !evdref
 
 let understand_judgment_tcc env evdref c =
-  let k0 = rel_context_length (rel_context env) in
+  let k0 = Context.Rel.length (rel_context env) in
   let j = pretype k0 true empty_tycon env evdref empty_lvar c in
   on_judgment (fun c ->
     let (evd,c) = process_inference_flags all_no_fail_flags env Evd.empty (!evdref,c) in
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 3f02e4bfb1..f59f880326 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -11,7 +11,6 @@ open Util
 open Names
 open Term
 open Vars
-open Context
 open Termops
 open Univ
 open Evd
@@ -1466,17 +1465,17 @@ let splay_prod_assum env sigma =
     match kind_of_term t with
     | Prod (x,t,c)  ->
 	prodec_rec (push_rel (x,None,t) env)
-	  (add_rel_decl (x, None, t) l) c
+	  (Context.Rel.add (x, None, t) l) c
     | LetIn (x,b,t,c) ->
 	prodec_rec (push_rel (x, Some b, t) env)
-	  (add_rel_decl (x, Some b, t) l) c
+	  (Context.Rel.add (x, Some b, t) l) c
     | Cast (c,_,_)    -> prodec_rec env l c
     | _               -> 
       let t' = whd_betadeltaiota env sigma t in
 	if Term.eq_constr t t' then l,t
 	else prodec_rec env l t'
   in
-  prodec_rec env empty_rel_context
+  prodec_rec env Context.Rel.empty
 
 let splay_arity env sigma c =
   let l, c = splay_prod env sigma c in
@@ -1491,20 +1490,20 @@ let splay_prod_n env sigma n =
     match kind_of_term (whd_betadeltaiota env sigma c) with
       | Prod (n,a,c0) ->
 	  decrec (push_rel (n,None,a) env)
-	    (m-1) (add_rel_decl (n,None,a) ln) c0
+	    (m-1) (Context.Rel.add (n,None,a) ln) c0
       | _                      -> invalid_arg "splay_prod_n"
   in
-  decrec env n empty_rel_context
+  decrec env n Context.Rel.empty
 
 let splay_lam_n env sigma n =
   let rec decrec env m ln c = if Int.equal m 0 then (ln,c) else
     match kind_of_term (whd_betadeltaiota env sigma c) with
       | Lambda (n,a,c0) ->
 	  decrec (push_rel (n,None,a) env)
-	    (m-1) (add_rel_decl (n,None,a) ln) c0
+	    (m-1) (Context.Rel.add (n,None,a) ln) c0
       | _                      -> invalid_arg "splay_lam_n"
   in
-  decrec env n empty_rel_context
+  decrec env n Context.Rel.empty
 
 let is_sort env sigma t =
   match kind_of_term (whd_betadeltaiota env sigma t) with
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 30c7ded243..55bce23089 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Univ
 open Evd
 open Environ
@@ -218,10 +217,10 @@ val splay_prod : env ->  evar_map -> constr -> (Name.t * constr) list * constr
 val splay_lam : env ->  evar_map -> constr -> (Name.t * constr) list * constr
 val splay_arity : env ->  evar_map -> constr -> (Name.t * constr) list * sorts
 val sort_of_arity : env -> evar_map -> constr -> sorts
-val splay_prod_n : env ->  evar_map -> int -> constr -> rel_context * constr
-val splay_lam_n : env ->  evar_map -> int -> constr -> rel_context * constr
+val splay_prod_n : env ->  evar_map -> int -> constr -> Context.Rel.t * constr
+val splay_lam_n : env ->  evar_map -> int -> constr -> Context.Rel.t * constr
 val splay_prod_assum :
-  env ->  evar_map -> constr -> rel_context * constr
+  env ->  evar_map -> constr -> Context.Rel.t * constr
 
 type 'a miota_args = {
   mP      : constr;     (** the result type *)
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 89ba46dbc4..70345c5092 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -8,7 +8,6 @@
 
 open Term
 open Evd
-open Context
 open Environ
 
 (** This family of functions assumes its constr argument is known to be
@@ -44,6 +43,6 @@ val type_of_global_reference_knowing_parameters : env -> evar_map -> constr ->
 val type_of_global_reference_knowing_conclusion :
   env -> evar_map -> constr -> types -> evar_map * types
 
-val sorts_of_context : env -> evar_map -> rel_context -> sorts list
+val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list
 
 val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index c44fbc0ba8..5595c3cdc2 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -12,7 +12,6 @@ open Globnames
 open Decl_kinds
 open Term
 open Vars
-open Context
 open Evd
 open Util
 open Typeclasses_errors
@@ -59,10 +58,10 @@ type typeclass = {
   cl_impl : global_reference;
 
   (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *)
-  cl_context : (global_reference * bool) option list * rel_context;
+  cl_context : (global_reference * bool) option list * Context.Rel.t;
 
   (* Context of definitions and properties on defs, will not be shared *)
-  cl_props : rel_context;
+  cl_props : Context.Rel.t;
 
   (* The method implementaions as projections. *)
   cl_projs : (Name.t * (direction * int option) option * constant option) list;
@@ -127,7 +126,7 @@ let typeclass_univ_instance (cl,u') =
     in Array.fold_left2 (fun subst u u' -> Univ.LMap.add u u' subst) 
       Univ.LMap.empty (Univ.Instance.to_array u) (Univ.Instance.to_array u')
   in
-  let subst_ctx = Context.map_rel_context (subst_univs_level_constr subst) in
+  let subst_ctx = Context.Rel.map (subst_univs_level_constr subst) in
     { cl with cl_context = fst cl.cl_context, subst_ctx (snd cl.cl_context);
       cl_props = subst_ctx cl.cl_props}, u'
 
@@ -204,7 +203,7 @@ let discharge_class (_,cl) =
 	(decl :: ctx', n :: subst)
     ) ctx ([], []) in
   let discharge_rel_context subst n rel =
-    let rel = map_rel_context (Cooking.expmod_constr repl) rel in
+    let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
     let ctx, _ =
       List.fold_right
 	(fun (id, b, t) (ctx, k) ->
@@ -287,7 +286,7 @@ let build_subclasses ~check env sigma glob pri =
       | None -> []
       | Some (rels, ((tc,u), args)) ->
 	let instapp = 
-	  Reductionops.whd_beta sigma (appvectc c (Context.extended_rel_vect 0 rels))
+	  Reductionops.whd_beta sigma (appvectc c (Context.Rel.to_extended_vect 0 rels))
 	in
 	let projargs = Array.of_list (args @ [instapp]) in
 	let projs = List.map_filter 
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index b3170b9702..f56af19a02 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -9,7 +9,6 @@
 open Names
 open Globnames
 open Term
-open Context
 open Evd
 open Environ
 
@@ -24,10 +23,10 @@ type typeclass = {
   (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses.
      The boolean indicates if the typeclass argument is a direct superclass and the global reference
      gives a direct link to the class itself. *)
-  cl_context : (global_reference * bool) option list * rel_context;
+  cl_context : (global_reference * bool) option list * Context.Rel.t;
 
   (** Context of definitions and properties on defs, will not be shared *)
-  cl_props : rel_context;
+  cl_props : Context.Rel.t;
 
   (** The methods implementations of the typeclass as projections. 
       Some may be undefinable due to sorting restrictions or simply undefined if 
@@ -68,7 +67,7 @@ val dest_class_app : env -> constr -> typeclass puniverses * constr list
 val typeclass_univ_instance : typeclass puniverses -> typeclass puniverses
 
 (** Just return None if not a class *)
-val class_of_constr : constr -> (rel_context * (typeclass puniverses * constr list)) option
+val class_of_constr : constr -> (Context.Rel.t * (typeclass puniverses * constr list)) option
   
 val instance_impl : instance -> global_reference
 
diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml
index 585f066db4..7a918ee876 100644
--- a/pretyping/typeclasses_errors.ml
+++ b/pretyping/typeclasses_errors.ml
@@ -9,7 +9,6 @@
 (*i*)
 open Names
 open Term
-open Context
 open Environ
 open Constrexpr
 open Globnames
@@ -20,7 +19,7 @@ type contexts = Parameters | Properties
 type typeclass_error =
     | NotAClass of constr
     | UnboundMethod of global_reference * Id.t Loc.located (* Class name, method *)
-    | MismatchedContextInstance of contexts * constr_expr list * rel_context (* found, expected *)
+    | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (* found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli
index 7982fc8524..b72d4db632 100644
--- a/pretyping/typeclasses_errors.mli
+++ b/pretyping/typeclasses_errors.mli
@@ -9,7 +9,6 @@
 open Loc
 open Names
 open Term
-open Context
 open Environ
 open Constrexpr
 open Globnames
@@ -19,7 +18,7 @@ type contexts = Parameters | Properties
 type typeclass_error =
   | NotAClass of constr
   | UnboundMethod of global_reference * Id.t located (** Class name, method *)
-  | MismatchedContextInstance of contexts * constr_expr list * rel_context (** found, expected *)
+  | MismatchedContextInstance of contexts * constr_expr list * Context.Rel.t (** found, expected *)
 
 exception TypeClassError of env * typeclass_error
 
@@ -27,5 +26,5 @@ val not_a_class : env -> constr -> 'a
 
 val unbound_method : env -> global_reference -> Id.t located -> 'a
 
-val mismatched_ctx_inst : env -> contexts -> constr_expr list -> rel_context -> 'a
+val mismatched_ctx_inst : env -> contexts -> constr_expr list -> Context.Rel.t -> 'a
 
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e8a0df4844..b42a70b340 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1582,7 +1582,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 occ test mkvarid d in
-        if Context.eq_named_declaration d newdecl
+        if Context.Named.Declaration.equal d newdecl
            && not (indirectly_dependent c d depdecls)
         then
           if check_occs && not (in_every_hyp occs)
@@ -1634,7 +1634,7 @@ type abstraction_request =
 
 type 'r abstraction_result =
   Names.Id.t * named_context_val *
-    Context.named_declaration list * Names.Id.t option *
+    Context.Named.Declaration.t list * Names.Id.t option *
     types * (constr, 'r) Sigma.sigma option
 
 let make_abstraction env evd ccl abs =
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 51a51f3752..14bcb4a06d 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -77,7 +77,7 @@ val finish_evar_resolution : ?flags:Pretyping.inference_flags ->
 
 type 'r abstraction_result =
   Names.Id.t * named_context_val *
-    Context.named_declaration list * Names.Id.t option *
+    Context.Named.Declaration.t list * Names.Id.t option *
     types * (constr, 'r) Sigma.sigma option
 
 val make_abstraction : env -> 'r Sigma.t -> constr ->
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c59e085e5b..38eea91700 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -53,7 +53,7 @@ let type_constructor mind mib u typ params =
   let s = ind_subst mind mib u in
   let ctyp = substl s typ in
   let ctyp = subst_instance_constr u ctyp in
-  let ndecls = Context.rel_context_length mib.mind_params_ctxt in
+  let ndecls = Context.Rel.length mib.mind_params_ctxt in
   if Int.equal ndecls 0 then ctyp
   else
     let _,ctyp = decompose_prod_n_assum ndecls ctyp in