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.

13 files changed, 112 insertions, 120 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4fb4b3263..a170c27fb 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -327,7 +327,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
           let env = Proofview.Goal.env gl in
           let nf c = Evarutil.nf_evar sigma c in
           let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
-          let hyp = Context.map_named_declaration nf decl in
+          let hyp = Context.Named.Declaration.map nf decl in
 	  let hintl = make_resolve_hyp env sigma hyp
 	  in trivial_fail_db dbg mod_delta db_list
 	       (Hint_db.add_list env sigma hintl local_db)
diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml
index 64a68ba6b..2c713a021 100644
--- a/tactics/eqschemes.ml
+++ b/tactics/eqschemes.ml
@@ -49,7 +49,6 @@ open Util
 open Names
 open Term
 open Vars
-open Context
 open Declarations
 open Environ
 open Inductive
@@ -71,8 +70,8 @@ let build_dependent_inductive ind (mib,mip) =
   let realargs,_ = List.chop mip.mind_nrealdecls mip.mind_arity_ctxt in
   applist
     (mkIndU ind,
-       extended_rel_list mip.mind_nrealdecls mib.mind_params_ctxt
-       @ extended_rel_list 0 realargs)
+       Context.Rel.to_extended_list mip.mind_nrealdecls mib.mind_params_ctxt
+       @ Context.Rel.to_extended_list 0 realargs)
 
 let my_it_mkLambda_or_LetIn s c = it_mkLambda_or_LetIn c s
 let my_it_mkProd_or_LetIn s c = it_mkProd_or_LetIn c s
@@ -109,7 +108,7 @@ let get_sym_eq_data env (ind,u) =
     error "Inductive equalities with local definitions in arity not supported.";
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
-  if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then
+  if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments"; (* This can be relaxed... *)
   let params,constrargs = List.chop mib.mind_nparams constrargs in
   if mip.mind_nrealargs > mib.mind_nparams then
@@ -144,7 +143,7 @@ let get_non_sym_eq_data env (ind,u) =
     error "Inductive equalities with local definitions in arity not supported";
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
-  if not (Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt)) then
+  if not (Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt)) then
     error "Constructor must have no arguments";
   let _,constrargs = List.chop mib.mind_nparams constrargs in
   let constrargs = List.map (Vars.subst_instance_constr u) constrargs in
@@ -170,7 +169,7 @@ let build_sym_scheme env ind =
   let (mib,mip as specif),nrealargs,realsign,paramsctxt,paramsctxt1 =
     get_sym_eq_data env indu in
   let cstr n =
-    mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in
+    mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let applied_ind = build_dependent_inductive indu specif in
   let realsign_ind =
@@ -183,7 +182,7 @@ let build_sym_scheme env ind =
      my_it_mkLambda_or_LetIn_name
        (lift_rel_context (nrealargs+1) realsign_ind)
        (mkApp (mkIndU indu,Array.concat
-	  [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+	  [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
 	   rel_vect 1 nrealargs;
 	   rel_vect (2*nrealargs+2) nrealargs])),
      mkRel 1 (* varH *),
@@ -224,13 +223,13 @@ let build_sym_involutive_scheme env ind =
     get_sym_eq_data env indu in
   let eq,eqrefl,ctx = get_coq_eq ctx in
   let sym, ctx, eff = const_of_scheme sym_scheme_kind env ind ctx in
-  let cstr n = mkApp (mkConstructUi (indu,1),extended_rel_vect n paramsctxt) in
+  let cstr n = mkApp (mkConstructUi (indu,1),Context.Rel.to_extended_vect n paramsctxt) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_C =
     mkApp
       (mkIndU indu, Array.append
-         (extended_rel_vect (nrealargs+1) mib.mind_params_ctxt)
+         (Context.Rel.to_extended_vect (nrealargs+1) mib.mind_params_ctxt)
          (rel_vect (nrealargs+1) nrealargs)) in
   let realsign_ind =
     name_context env ((Name varH,None,applied_ind)::realsign) in
@@ -244,15 +243,15 @@ let build_sym_involutive_scheme env ind =
 	       (mkApp (eq,[|
 	       mkApp
 	       (mkIndU indu, Array.concat
-	       [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+	       [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
 		rel_vect (2*nrealargs+2) nrealargs;
 		rel_vect 1 nrealargs]);
                mkApp (sym,Array.concat
-	       [extended_rel_vect (3*nrealargs+2) paramsctxt1;
+	       [Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
 		rel_vect 1 nrealargs;
 		rel_vect (2*nrealargs+2) nrealargs;
 		[|mkApp (sym,Array.concat
-		[extended_rel_vect (3*nrealargs+2) paramsctxt1;
+		[Context.Rel.to_extended_vect (3*nrealargs+2) paramsctxt1;
 		 rel_vect (2*nrealargs+2) nrealargs;
 		 rel_vect 1 nrealargs;
 		 [|mkRel 1|]])|]]);
@@ -335,7 +334,7 @@ let build_l2r_rew_scheme dep env ind kind =
   let eq,eqrefl,ctx = get_coq_eq ctx in
   let cstr n p =
     mkApp (mkConstructUi(indu,1),
-      Array.concat [extended_rel_vect n paramsctxt1;
+      Array.concat [Context.Rel.to_extended_vect n paramsctxt1;
                     rel_vect p nrealargs]) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -343,12 +342,12 @@ let build_l2r_rew_scheme dep env ind kind =
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_P =
     mkApp (mkIndU indu, Array.concat
-       [extended_rel_vect (3*nrealargs) paramsctxt1;
+       [Context.Rel.to_extended_vect (3*nrealargs) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect nrealargs nrealargs]) in
   let applied_ind_G =
     mkApp (mkIndU indu, Array.concat
-       [extended_rel_vect (3*nrealargs+3) paramsctxt1;
+       [Context.Rel.to_extended_vect (3*nrealargs+3) paramsctxt1;
         rel_vect (nrealargs+3) nrealargs;
         rel_vect 0 nrealargs]) in
   let realsign_P = lift_rel_context nrealargs realsign in
@@ -359,10 +358,10 @@ let build_l2r_rew_scheme dep env ind kind =
                       lift_rel_context (nrealargs+3) realsign) in
   let applied_sym_C n =
      mkApp(sym,
-       Array.append (extended_rel_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in
+       Array.append (Context.Rel.to_extended_vect n mip.mind_arity_ctxt) [|mkVar varH|]) in
   let applied_sym_G =
      mkApp(sym,
-       Array.concat [extended_rel_vect (nrealargs*3+4) paramsctxt1;
+       Array.concat [Context.Rel.to_extended_vect (nrealargs*3+4) paramsctxt1;
                      rel_vect (nrealargs+4) nrealargs;
                      rel_vect 1 nrealargs;
 		     [|mkRel 1|]]) in
@@ -372,7 +371,7 @@ let build_l2r_rew_scheme dep env ind kind =
   let ci = make_case_info (Global.env()) ind RegularStyle in
   let cieq = make_case_info (Global.env()) (fst (destInd eq)) RegularStyle in
   let applied_PC =
-    mkApp (mkVar varP,Array.append (extended_rel_vect 1 realsign)
+    mkApp (mkVar varP,Array.append (Context.Rel.to_extended_vect 1 realsign)
            (if dep then [|cstr (2*nrealargs+1) 1|] else [||])) in
   let applied_PG =
     mkApp (mkVar varP,Array.append (rel_vect 1 nrealargs)
@@ -382,11 +381,11 @@ let build_l2r_rew_scheme dep env ind kind =
            (if dep then [|mkRel 2|] else [||])) in
   let applied_sym_sym =
          mkApp (sym,Array.concat
-	   [extended_rel_vect (2*nrealargs+4) paramsctxt1;
+	   [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1;
             rel_vect 4 nrealargs;
             rel_vect (nrealargs+4) nrealargs;
             [|mkApp (sym,Array.concat
-	      [extended_rel_vect (2*nrealargs+4) paramsctxt1;
+	      [Context.Rel.to_extended_vect (2*nrealargs+4) paramsctxt1;
 	       rel_vect (nrealargs+4) nrealargs;
 	       rel_vect 4 nrealargs;
 	       [|mkRel 2|]])|]]) in
@@ -409,7 +408,7 @@ let build_l2r_rew_scheme dep env ind kind =
                    mkApp (eq,[|lift 4 applied_ind;applied_sym_sym;mkRel 1|]),
                    applied_PR)),
        mkApp (sym_involutive,
-         Array.append (extended_rel_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]),
+         Array.append (Context.Rel.to_extended_vect 3 mip.mind_arity_ctxt) [|mkVar varH|]),
        [|main_body|])
    else
      main_body))))))
@@ -448,7 +447,7 @@ let build_l2r_forward_rew_scheme dep env ind kind =
     get_sym_eq_data env indu in
   let cstr n p =
     mkApp (mkConstructUi(indu,1),
-      Array.concat [extended_rel_vect n paramsctxt1;
+      Array.concat [Context.Rel.to_extended_vect n paramsctxt1;
                     rel_vect p nrealargs]) in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -456,12 +455,12 @@ let build_l2r_forward_rew_scheme dep env ind kind =
   let applied_ind = build_dependent_inductive indu specif in
   let applied_ind_P =
     mkApp (mkIndU indu, Array.concat
-       [extended_rel_vect (4*nrealargs+2) paramsctxt1;
+       [Context.Rel.to_extended_vect (4*nrealargs+2) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect (nrealargs+1) nrealargs]) in
   let applied_ind_P' =
     mkApp (mkIndU indu, Array.concat
-       [extended_rel_vect (3*nrealargs+1) paramsctxt1;
+       [Context.Rel.to_extended_vect (3*nrealargs+1) paramsctxt1;
         rel_vect 0 nrealargs;
         rel_vect (2*nrealargs+1) nrealargs]) in
   let realsign_P n = lift_rel_context (nrealargs*n+n) realsign in
@@ -539,7 +538,7 @@ let build_r2l_forward_rew_scheme dep env ind kind =
   let ((mib,mip as specif),constrargs,realsign,paramsctxt,nrealargs) =
     get_non_sym_eq_data env indu in
   let cstr n =
-    mkApp (mkConstructUi(indu,1),extended_rel_vect n mib.mind_params_ctxt) in
+    mkApp (mkConstructUi(indu,1),Context.Rel.to_extended_vect n mib.mind_params_ctxt) in
   let constrargs_cstr = constrargs@[cstr 0] in
   let varH = fresh env (default_id_of_sort (snd (mind_arity mip))) in
   let varHC = fresh env (Id.of_string "HC") in
@@ -555,8 +554,8 @@ let build_r2l_forward_rew_scheme dep env ind kind =
     applist (mkVar varP,if dep then constrargs_cstr else constrargs) in
   let applied_PG =
     mkApp (mkVar varP,
-           if dep then extended_rel_vect 0 realsign_ind
-	   else extended_rel_vect 1 realsign) in
+           if dep then Context.Rel.to_extended_vect 0 realsign_ind
+	   else Context.Rel.to_extended_vect 1 realsign) in
   let c = 
   (my_it_mkLambda_or_LetIn paramsctxt
   (my_it_mkLambda_or_LetIn_name realsign_ind
@@ -600,12 +599,12 @@ let fix_r2l_forward_rew_scheme (c, ctx') =
   | hp :: p :: ind :: indargs ->
      let c' = 
       my_it_mkLambda_or_LetIn indargs
-	(mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 1) p)
-	  (mkLambda_or_LetIn (map_rel_declaration (liftn (-1) 2) hp)
-	    (mkLambda_or_LetIn (map_rel_declaration (lift 2) ind)
+	(mkLambda_or_LetIn (Context.Rel.Declaration.map (liftn (-1) 1) p)
+	  (mkLambda_or_LetIn (Context.Rel.Declaration.map (liftn (-1) 2) hp)
+	    (mkLambda_or_LetIn (Context.Rel.Declaration.map (lift 2) ind)
 	      (Reductionops.whd_beta Evd.empty
 		(applist (c,
-	          extended_rel_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
+	          Context.Rel.to_extended_list 3 indargs @ [mkRel 1;mkRel 3;mkRel 2]))))))
       in c', ctx'
   | _ -> anomaly (Pp.str "Ill-formed non-dependent left-to-right rewriting scheme")
 
@@ -744,7 +743,7 @@ let build_congr env (eq,refl,ctx) ind =
   let (_,_,ty) = lookup_rel (mip.mind_nrealargs - i + 1) env_with_arity in
   let constrsign,ccl = decompose_prod_assum mip.mind_nf_lc.(0) in
   let _,constrargs = decompose_app ccl in
-  if Int.equal (rel_context_length constrsign) (rel_context_length mib.mind_params_ctxt) then
+  if Int.equal (Context.Rel.length constrsign) (Context.Rel.length mib.mind_params_ctxt) then
     error "Constructor must have no arguments";
   let b = List.nth constrargs (i + mib.mind_nparams - 1) in
   let varB = fresh env (Id.of_string "B") in
@@ -760,8 +759,8 @@ let build_congr env (eq,refl,ctx) ind =
      (mkNamedLambda varH
         (applist
            (mkIndU indu,
-	    extended_rel_list (mip.mind_nrealargs+2) paramsctxt @
-	    extended_rel_list 0 realsign))
+	    Context.Rel.to_extended_list (mip.mind_nrealargs+2) paramsctxt @
+	    Context.Rel.to_extended_list 0 realsign))
      (mkCase (ci,
        my_it_mkLambda_or_LetIn_name
 	 (lift_rel_context (mip.mind_nrealargs+3) realsign)
@@ -769,9 +768,9 @@ let build_congr env (eq,refl,ctx) ind =
            (Anonymous,
             applist
              (mkIndU indu,
-	        extended_rel_list (2*mip.mind_nrealdecls+3)
+	        Context.Rel.to_extended_list (2*mip.mind_nrealdecls+3)
 		  paramsctxt
-	        @ extended_rel_list 0 realsign),
+	        @ Context.Rel.to_extended_list 0 realsign),
             mkApp (eq,
 	      [|mkVar varB;
                 mkApp (mkVar varf, [|lift (2*mip.mind_nrealdecls+4) b|]);
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 92ebcb272..7d15e9ee6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1574,7 +1574,7 @@ let unfold_body x =
   Proofview.Goal.enter { enter = begin fun gl ->
   (** We normalize the given hypothesis immediately. *)
   let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
-  let (_, xval, _) = Context.lookup_named x hyps in
+  let (_, xval, _) = Context.Named.lookup x hyps in
   let xval = match xval with
   | None -> errorlabstrm "unfold_body"
     (pr_id x ++ str" is not a defined hypothesis.")
@@ -1656,7 +1656,7 @@ let subst_one_var dep_proof_ok x =
           (** [is_eq_x] ensures nf_evar on its side *)
           let hyps = Proofview.Goal.hyps gl in
           let test hyp _ = is_eq_x gl varx hyp in
-          Context.fold_named_context test ~init:() hyps;
+          Context.Named.fold_outside test ~init:() hyps;
           errorlabstrm "Subst"
             (str "Cannot find any non-recursive equality over " ++ pr_id x ++
 	       str".")
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 92682fc7a..f311e47f6 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -315,7 +315,7 @@ let project_hint pri l2r r =
     | _ -> assert false in
   let p =
     if l2r then build_coq_iff_left_proj () else build_coq_iff_right_proj () in
-  let c = Reductionops.whd_beta Evd.empty (mkApp (c,Context.extended_rel_vect 0 sign)) in
+  let c = Reductionops.whd_beta Evd.empty (mkApp (c, Context.Rel.to_extended_vect 0 sign)) in
   let c = it_mkLambda_or_LetIn
     (mkApp (p,[|mkArrow a (lift 1 b);mkArrow b (lift 1 a);c|])) sign in
   let id =
diff --git a/tactics/hints.mli b/tactics/hints.mli
index 3a0521f66..b48fb776e 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -10,7 +10,6 @@ open Pp
 open Util
 open Names
 open Term
-open Context
 open Environ
 open Globnames
 open Decl_kinds
@@ -192,7 +191,7 @@ val make_resolves :
    If the hyp cannot be used as a Hint, the empty list is returned. *)
 
 val make_resolve_hyp :
-  env -> evar_map -> named_declaration -> hint_entry list
+  env -> evar_map -> Context.Named.Declaration.t -> hint_entry list
 
 (** [make_extern pri pattern tactic_expr] *)
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index ed1a62795..3574990f6 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -13,7 +13,6 @@ open Names
 open Nameops
 open Term
 open Vars
-open Context
 open Termops
 open Namegen
 open Environ
@@ -97,7 +96,7 @@ let make_inv_predicate env evd indf realargs id status concl =
 	  (* We lift to make room for the equations *)
 	  (hyps,lift nrealargs bodypred)
   in
-  let nhyps = rel_context_length hyps in
+  let nhyps = Context.Rel.length hyps in
   let env' = push_rel_context hyps env in
   (* Now the arity is pushed, and we need to construct the pairs
    * ai,mkRel(n-i+1) *)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 75e69bc09..9154c50c8 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -14,7 +14,6 @@ open Term
 open Vars
 open Termops
 open Namegen
-open Context
 open Evd
 open Printer
 open Reductionops
@@ -157,7 +156,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option =
 	fold_named_context
 	  (fun env (id,_,_ as d) (revargs,hyps) ->
              if Id.List.mem id ivars then
-	       ((mkVar id)::revargs,add_named_decl d hyps)
+	       ((mkVar id)::revargs, Context.Named.add d hyps)
 	     else
 	       (revargs,hyps))
           env ~init:([],[])
@@ -206,8 +205,8 @@ let inversion_scheme env sigma t sort dep_option inv_op =
     fold_named_context
       (fun env (id,_,_ as d) sign ->
          if mem_named_context id global_named_context then sign
-	 else add_named_decl d sign)
-      invEnv ~init:empty_named_context
+	 else Context.Named.add d sign)
+      invEnv ~init:Context.Named.empty
   end in
   let avoid = ref [] in
   let { sigma=sigma } = Proof.V82.subgoals pf in
@@ -218,7 +217,7 @@ let inversion_scheme env sigma t sort dep_option inv_op =
 	let h = next_ident_away (Id.of_string "H") !avoid in
 	let ty,inst = Evarutil.generalize_evar_over_rels sigma (e,args) in
 	avoid := h::!avoid;
-	ownSign := add_named_decl (h,None,ty) !ownSign;
+	ownSign := Context.Named.add (h,None,ty) !ownSign;
 	applist (mkVar h, inst)
     | _ -> map_constr fill_holes c
   in
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index 40a18ac45..1de47b2be 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -71,7 +71,7 @@ val cl_rewrite_clause :
   bool -> Locus.occurrences -> Id.t option -> tactic
 
 val is_applied_rewrite_relation :
-  env -> evar_map -> Context.rel_context -> constr -> types option
+  env -> evar_map -> Context.Rel.t -> constr -> types option
 
 val declare_relation :
   ?binders:local_binder list -> constr_expr -> constr_expr -> Id.t ->
diff --git a/tactics/tactic_matching.mli b/tactics/tactic_matching.mli
index d8e6dd0ae..090207bcc 100644
--- a/tactics/tactic_matching.mli
+++ b/tactics/tactic_matching.mli
@@ -43,7 +43,7 @@ val match_term :
 val match_goal:
   Environ.env ->
   Evd.evar_map ->
-  Context.named_context ->
+  Context.Named.t ->
   Term.constr ->
   (Tacexpr.binding_bound_vars * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule list ->
   Tacexpr.glob_tactic_expr t Proofview.tactic
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index e181c8e14..aaef0f072 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -12,7 +12,6 @@ open Util
 open Names
 open Term
 open Termops
-open Context
 open Declarations
 open Tacmach
 open Clenv
@@ -154,8 +153,8 @@ type branch_args = {
   branchnames : Tacexpr.intro_patterns}
 
 type branch_assumptions = {
-  ba        : branch_args;     (* the branch args *)
-  assums    : named_context}   (* the list of assumptions introduced *)
+  ba        : branch_args;       (* the branch args *)
+  assums    : Context.Named.t}   (* the list of assumptions introduced *)
 
 let fix_empty_or_and_pattern nv l =
   (* 1- The syntax does not distinguish between "[ ]" for one clause with no
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 80e01a8d0..d8aa3161e 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -9,7 +9,6 @@
 open Pp
 open Names
 open Term
-open Context
 open Tacmach
 open Proof_type
 open Tacexpr
@@ -60,29 +59,29 @@ val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic
 
 val onNthHypId       : int -> (Id.t -> tactic) -> tactic
 val onNthHyp         : int -> (constr -> tactic) -> tactic
-val onNthDecl        : int -> (named_declaration -> tactic) -> tactic
+val onNthDecl        : int -> (Context.Named.Declaration.t -> tactic) -> tactic
 val onLastHypId      : (Id.t -> tactic) -> tactic
 val onLastHyp        : (constr -> tactic) -> tactic
-val onLastDecl       : (named_declaration -> tactic) -> tactic
+val onLastDecl       : (Context.Named.Declaration.t -> tactic) -> tactic
 val onNLastHypsId    : int -> (Id.t list -> tactic) -> tactic
 val onNLastHyps      : int -> (constr list -> tactic) -> tactic
-val onNLastDecls     : int -> (named_context -> tactic) -> tactic
+val onNLastDecls     : int -> (Context.Named.t -> tactic) -> tactic
 
 val lastHypId   : goal sigma -> Id.t
 val lastHyp     : goal sigma -> constr
-val lastDecl    : goal sigma -> named_declaration
+val lastDecl    : goal sigma -> Context.Named.Declaration.t
 val nLastHypsId : int -> goal sigma -> Id.t list
 val nLastHyps   : int -> goal sigma -> constr list
-val nLastDecls  : int -> goal sigma -> named_context
+val nLastDecls  : int -> goal sigma -> Context.Named.t
 
-val afterHyp    : Id.t -> goal sigma -> named_context
+val afterHyp    : Id.t -> goal sigma -> Context.Named.t
 
 val ifOnHyp     : (Id.t * types -> bool) ->
                   (Id.t -> tactic) -> (Id.t -> tactic) ->
 		   Id.t -> tactic
 
-val onHyps      : (goal sigma -> named_context) ->
-                  (named_context -> tactic) -> tactic
+val onHyps      : (goal sigma -> Context.Named.t) ->
+                  (Context.Named.t -> tactic) -> tactic
 
 (** {6 Tacticals applying to goal components } *)
 
@@ -99,18 +98,18 @@ val onClauseLR : (Id.t option -> tactic) -> clause -> tactic
 (** {6 Elimination tacticals. } *)
 
 type branch_args = {
-  ity        : pinductive;   (** the type we were eliminating on *)
+  ity        : pinductive;  (** the type we were eliminating on *)
   largs      : constr list; (** its arguments *)
   branchnum  : int;         (** the branch number *)
   pred       : constr;      (** the predicate we used *)
   nassums    : int;         (** the number of assumptions to be introduced *)
   branchsign : bool list;   (** the signature of the branch.
-                               true=recursive argument, false=constant *)
+                                true=recursive argument, false=constant *)
   branchnames : intro_patterns}
 
 type branch_assumptions = {
-  ba        : branch_args;     (** the branch args *)
-  assums    : named_context}   (** the list of assumptions introduced *)
+  ba        : branch_args;       (** the branch args *)
+  assums    : Context.Named.t}   (** the list of assumptions introduced *)
 
 (** [check_disjunctive_pattern_size loc pats n] returns an appropriate 
    error message if |pats| <> n *)
@@ -223,7 +222,7 @@ module New : sig
   val tclTIMEOUT : int -> unit tactic -> unit tactic
   val tclTIME : string option -> 'a tactic -> 'a tactic
 
-  val nLastDecls  : ([ `NF ], 'r) Proofview.Goal.t -> int -> named_context
+  val nLastDecls  : ([ `NF ], 'r) Proofview.Goal.t -> int -> Context.Named.t
 
   val ifOnHyp     : (identifier * types -> bool) ->
     (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) ->
@@ -232,11 +231,11 @@ module New : sig
   val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic
   val onLastHypId      : (identifier -> unit tactic) -> unit tactic
   val onLastHyp        : (constr -> unit tactic) -> unit tactic
-  val onLastDecl       : (named_declaration -> unit tactic) -> unit tactic
+  val onLastDecl       : (Context.Named.Declaration.t -> unit tactic) -> unit tactic
 
-  val onHyps      : ([ `NF ], named_context) Proofview.Goal.enter ->
-                    (named_context -> unit tactic) -> unit tactic
-  val afterHyp    : Id.t -> (named_context -> unit tactic) -> unit tactic
+  val onHyps      : ([ `NF ], Context.Named.t) Proofview.Goal.enter ->
+                    (Context.Named.t -> unit tactic) -> unit tactic
+  val afterHyp    : Id.t -> (Context.Named.t -> unit tactic) -> unit tactic
 
   val tryAllHyps          : (identifier -> unit tactic) -> unit tactic
   val tryAllHypsAndConcl  : (identifier option -> unit tactic) -> unit tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2e7adc513..f2319804e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -13,7 +13,6 @@ open Names
 open Nameops
 open Term
 open Vars
-open Context
 open Termops
 open Find_subterm
 open Namegen
@@ -1405,7 +1404,7 @@ let make_projection env sigma params cstr sign elim i n c u =
       then
         let t = lift (i+1-n) t in
 	let abselim = beta_applist (elim,params@[t;branch]) in
-	let c = beta_applist (abselim, [mkApp (c, extended_rel_vect 0 sign)]) in
+	let c = beta_applist (abselim, [mkApp (c, Context.Rel.to_extended_vect 0 sign)]) in
 	  Some (it_mkLambda_or_LetIn c sign, it_mkProd_or_LetIn t sign)
       else
 	None
@@ -1413,7 +1412,7 @@ let make_projection env sigma params cstr sign elim i n c u =
       (* goes from left to right when i increases! *)
       match List.nth l i with
       | Some proj ->
-	  let args = extended_rel_vect 0 sign in
+	  let args = Context.Rel.to_extended_vect 0 sign in
 	  let proj =
 	    if Environ.is_projection proj env then
 	      mkProj (Projection.make proj false, mkApp (c, args))
@@ -2528,7 +2527,7 @@ let bring_hyps hyps =
       let store = Proofview.Goal.extra gl in
       let concl = Tacmach.New.pf_nf_concl gl in
       let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
-      let args = Array.of_list (instance_from_named_context hyps) in
+      let args = Array.of_list (Context.Named.to_instance hyps) in
       Proofview.Refine.refine { run = begin fun sigma ->
         let Sigma (ev, sigma, p) =
           Evarutil.new_evar env sigma ~principal:true ~store newcl in
@@ -2589,7 +2588,7 @@ let generalize_dep ?(with_let=false) c gl =
       d::toquant
     else
       toquant in
-  let to_quantify = Context.fold_named_context seek sign ~init:[] in
+  let to_quantify = Context.Named.fold_outside seek sign ~init:[] in
   let to_quantify_rev = List.rev to_quantify in
   let qhyps = List.map (fun (id,_,_) -> id) to_quantify_rev in
   let tothin = List.filter (fun id -> not (Id.List.mem id init_ids)) qhyps in
@@ -2609,7 +2608,7 @@ let generalize_dep ?(with_let=false) c gl =
   in
   let cl'',evd = generalize_goal gl 0 ((AllOccurrences,c,body),Anonymous)
     (cl',project gl) in
-  let args = instance_from_named_context to_quantify_rev in
+  let args = Context.Named.to_instance to_quantify_rev in
   tclTHENLIST
     [tclEVARS evd;
      apply_type cl'' (if Option.is_empty body then c::args else args);
@@ -2687,7 +2686,7 @@ let quantify lconstr =
 let unfold_body x gl =
   let hyps = pf_hyps gl in
   let xval =
-    match Context.lookup_named x hyps with
+    match Context.Named.lookup x hyps with
         (_,Some xval,_) -> xval
       | _ -> errorlabstrm "unfold_body"
           (pr_id x ++ str" is not a defined hypothesis.") in
@@ -3108,20 +3107,20 @@ type elim_scheme = {
   elimc: constr with_bindings option;
   elimt: types;
   indref: global_reference option;
-  params: rel_context;     (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
-  nparams: int;            (* number of parameters *)
-  predicates: rel_context; (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
-  npredicates: int;        (* Number of predicates *)
-  branches: rel_context;   (* branchr,...,branch1 *)
-  nbranches: int;          (* Number of branches *)
-  args: rel_context;       (* (xni, Ti_ni) ... (x1, Ti_1) *)
-  nargs: int;              (* number of arguments *)
-  indarg: rel_declaration option; (* Some (H,I prm1..prmp x1...xni)
-				     if HI is in premisses, None otherwise *)
-  concl: types;            (* Qi x1...xni HI (f...), HI and (f...)
-			      are optional and mutually exclusive *)
-  indarg_in_concl: bool;   (* true if HI appears at the end of conclusion *)
-  farg_in_concl: bool;     (* true if (f...) appears at the end of conclusion *)
+  params: Context.Rel.t;      (* (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
+  nparams: int;               (* number of parameters *)
+  predicates: Context.Rel.t;  (* (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
+  npredicates: int;           (* Number of predicates *)
+  branches: Context.Rel.t;    (* branchr,...,branch1 *)
+  nbranches: int;             (* Number of branches *)
+  args: Context.Rel.t;        (* (xni, Ti_ni) ... (x1, Ti_1) *)
+  nargs: int;                 (* number of arguments *)
+  indarg: Context.Rel.Declaration.t option; (* Some (H,I prm1..prmp x1...xni)
+                                               if HI is in premisses, None otherwise *)
+  concl: types;               (* Qi x1...xni HI (f...), HI and (f...)
+			         are optional and mutually exclusive *)
+  indarg_in_concl: bool;      (* true if HI appears at the end of conclusion *)
+  farg_in_concl: bool;        (* true if (f...) appears at the end of conclusion *)
 }
 
 let empty_scheme =
@@ -3280,7 +3279,7 @@ let hyps_of_vars env sign nogen hyps =
   if Id.Set.is_empty hyps then []
   else
     let (_,lh) =
-      Context.fold_named_context_reverse
+      Context.Named.fold_inside
         (fun (hs,hl) (x,_,_ as d) ->
 	  if Id.Set.mem x nogen then (hs,hl)
 	  else if Id.Set.mem x hs then (hs,x::hl)
@@ -3511,7 +3510,7 @@ let occur_rel n c =
    We also return the conclusion.
 *)
 let decompose_paramspred_branch_args elimt =
-  let rec cut_noccur elimt acc2 : rel_context * rel_context * types =
+  let rec cut_noccur elimt acc2 : Context.Rel.t * Context.Rel.t * types =
     match kind_of_term elimt with
       | Prod(nme,tpe,elimt') ->
 	  let hd_tpe,_ = decompose_app ((strip_prod_assum tpe)) in
@@ -3520,7 +3519,7 @@ let decompose_paramspred_branch_args elimt =
 	  else let acc3,ccl = decompose_prod_assum elimt in acc2 , acc3 , ccl
       | App(_, _) | Rel _ -> acc2 , [] , elimt
       | _ -> error_ind_scheme "" in
-  let rec cut_occur elimt acc1 : rel_context * rel_context * rel_context * types =
+  let rec cut_occur elimt acc1 : Context.Rel.t * Context.Rel.t * Context.Rel.t * types =
     match kind_of_term elimt with
       | Prod(nme,tpe,c) when occur_rel 1 c -> cut_occur c ((nme,None,tpe)::acc1)
       | Prod(nme,tpe,c) -> let acc2,acc3,ccl = cut_noccur elimt [] in acc1,acc2,acc3,ccl
@@ -3648,7 +3647,7 @@ let compute_scheme_signature scheme names_info ind_type_guess =
 	    let ind_is_ok =
 	      List.equal Term.eq_constr
 		(List.lastn scheme.nargs indargs)
-		(extended_rel_list 0 scheme.args) in
+		(Context.Rel.to_extended_list 0 scheme.args) in
 	    if not (ccl_arg_ok && ind_is_ok) then
 	      error_ind_scheme "the conclusion of"
 	  in (cond, check_concl)
@@ -4563,10 +4562,10 @@ let abstract_subproof id gk tac =
     List.fold_right
       (fun (id,_,_ as d) (s1,s2) ->
 	if mem_named_context id current_sign &&
-          interpretable_as_section_decl evdref (Context.lookup_named id current_sign) d
+          interpretable_as_section_decl evdref (Context.Named.lookup id current_sign) d
         then (s1,push_named_context_val d s2)
-	else (add_named_decl d s1,s2))
-      global_sign (empty_named_context,empty_named_context_val) in
+	else (Context.Named.add d s1,s2))
+      global_sign (Context.Named.empty, empty_named_context_val) in
   let id = next_global_ident_away id (pf_ids_of_hyps gl) in
   let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in
   let concl =
@@ -4594,7 +4593,7 @@ let abstract_subproof id gk tac =
   in
   let const, args =
     if !shrink_abstract then shrink_entry sign const
-    else (const, List.rev (instance_from_named_context sign))
+    else (const, List.rev (Context.Named.to_instance sign))
   in
   let cd = Entries.DefinitionEntry const in
   let decl = (cd, IsProof Lemma) in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index f5695ff06..873a11bd2 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -9,7 +9,6 @@
 open Loc
 open Names
 open Term
-open Context
 open Environ
 open Proof_type
 open Evd
@@ -33,9 +32,9 @@ val is_quantified_hypothesis : Id.t -> goal sigma -> bool
 val introduction    : ?check:bool -> Id.t -> unit Proofview.tactic
 val refine          : constr -> tactic
 val convert_concl   : ?check:bool -> types -> cast_kind -> unit Proofview.tactic
-val convert_hyp     : ?check:bool -> named_declaration -> unit Proofview.tactic
+val convert_hyp     : ?check:bool -> Context.Named.Declaration.t -> unit Proofview.tactic
 val convert_concl_no_check : types -> cast_kind -> unit Proofview.tactic
-val convert_hyp_no_check : named_declaration -> unit Proofview.tactic
+val convert_hyp_no_check : Context.Named.Declaration.t -> unit Proofview.tactic
 val thin            : Id.t list -> tactic
 val mutual_fix      :
   Id.t -> int -> (Id.t * int * constr) list -> int -> tactic
@@ -50,7 +49,7 @@ val convert_leq     : constr -> constr -> unit Proofview.tactic
 
 val fresh_id_in_env : Id.t list -> Id.t -> env -> Id.t
 val fresh_id : Id.t list -> Id.t -> goal sigma -> Id.t
-val find_intro_names : rel_context -> goal sigma -> Id.t list
+val find_intro_names : Context.Rel.t -> goal sigma -> Id.t list
 
 val intro                : unit Proofview.tactic
 val introf               : unit Proofview.tactic
@@ -180,7 +179,7 @@ val revert        : Id.t list -> unit Proofview.tactic
 (** {6 Resolution tactics. } *)
 
 val apply_type : constr -> constr list -> tactic
-val bring_hyps : named_context -> unit Proofview.tactic
+val bring_hyps : Context.Named.t -> unit Proofview.tactic
 
 val apply                 : constr -> unit Proofview.tactic
 val eapply                : constr -> unit Proofview.tactic
@@ -239,20 +238,20 @@ type elim_scheme = {
   elimc: constr with_bindings option;
   elimt: types;
   indref: global_reference option;
-  params: rel_context;     (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
-  nparams: int;            (** number of parameters *)
-  predicates: rel_context; (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
-  npredicates: int;        (** Number of predicates *)
-  branches: rel_context;   (** branchr,...,branch1 *)
-  nbranches: int;          (** Number of branches *)
-  args: rel_context;       (** (xni, Ti_ni) ... (x1, Ti_1) *)
-  nargs: int;              (** number of arguments *)
-  indarg: rel_declaration option; (** Some (H,I prm1..prmp x1...xni)
-				     if HI is in premisses, None otherwise *)
-  concl: types;            (** Qi x1...xni HI (f...), HI and (f...)
-			      are optional and mutually exclusive *)
-  indarg_in_concl: bool;   (** true if HI appears at the end of conclusion *)
-  farg_in_concl: bool;     (** true if (f...) appears at the end of conclusion *)
+  params: Context.Rel.t;      (** (prm1,tprm1);(prm2,tprm2)...(prmp,tprmp) *)
+  nparams: int;               (** number of parameters *)
+  predicates: Context.Rel.t;  (** (Qq, (Tq_1 -> Tq_2 ->...-> Tq_nq)), (Q1,...) *)
+  npredicates: int;           (** Number of predicates *)
+  branches: Context.Rel.t;    (** branchr,...,branch1 *)
+  nbranches: int;             (** Number of branches *)
+  args: Context.Rel.t;        (** (xni, Ti_ni) ... (x1, Ti_1) *)
+  nargs: int;                 (** number of arguments *)
+  indarg: Context.Rel.Declaration.t option;  (** Some (H,I prm1..prmp x1...xni)
+	  		 	                 if HI is in premisses, None otherwise *)
+  concl: types;               (** Qi x1...xni HI (f...), HI and (f...)
+			          are optional and mutually exclusive *)
+  indarg_in_concl: bool;      (** true if HI appears at the end of conclusion *)
+  farg_in_concl: bool;        (** true if (f...) appears at the end of conclusion *)
 }
 
 val compute_elim_sig : ?elimc: constr with_bindings -> types -> elim_scheme