CLEANUP: kernel/context.ml{,i}

The structure of the Context module was refined in such a way that:
- Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module.
- Types and functions related to rel-context were put into the Context.Rel module.
- Types and functions related to named-context declarations were put into the Context.Named.Declaration module.
- Types and functions related to named-context were put into the Context.Named module.
- Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module.
- Types and functions related to named-list-context were put into Context.NamedList module.

Some missing comments were added to the *.mli file.

The output of ocamldoc was checked whether it looks in a reasonable way.

"TODO: cleanup" was removed

The order in which are exported functions listed in the *.mli file was changed.
(as in a mature modules, this order usually is not random)

The order of exported functions in Context.{Rel,Named} modules is now consistent.
(as there is no special reason why that order should be different)

The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file.
(as there is no special reason to define them in a different order)

The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do.
(Now they are called Context.{Rel,Named}.fold_{inside,outside})

The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated.

Thrown exceptions are now documented.

Naming of formal parameters was made more consistent across different functions.

Comments of similar functions in different modules are now consistent.

Comments from *.mli files were copied to *.ml file.
(We need that information in *.mli files because that is were ocamldoc needs it.
 It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function,
 we can see the comments also there and do not need to open a different file if we want to see it.)

When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1.
(UTF-8 characters are used in our ocamldoc markup)

"open Context" was removed from all *.mli and *.ml files.
(Originally, it was OK to do that. Now it is not.)

An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.

24 files changed, 113 insertions, 134 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 fe26dcd282..c6c397135a 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/patternops.mli b/pretyping/patternops.mli
index 0148280287..34191db344 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -6,7 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Context
 open Term
 open Globnames
 open Glob_term
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index ce6d189855..6d9ed9a30c 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
@@ -529,14 +528,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 ->
@@ -563,7 +562,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
@@ -884,7 +883,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 =
@@ -1017,7 +1016,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
@@ -1059,7 +1058,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 
@@ -1067,7 +1066,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 43c98bbd47..5195784a4c 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
 val is_sort : env -> evar_map -> types -> bool
 
 type 'a miota_args = {
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 deb03f5160..c4f22987f7 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