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, 32 insertions, 41 deletions

diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index a71588fe05..4704854384 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -141,7 +141,7 @@ let label_of = function
   | ConstructRef ((kn,_),_) -> pi3 (repr_mind kn)
   | VarRef id -> Label.of_id id
 
-let push (r : Context.rel_declaration) (ctx : Context.rel_context) = r :: ctx
+let push (r : Context.Rel.Declaration.t) (ctx : Context.Rel.t) = r :: ctx
 
 let rec traverse current ctx accu t = match kind_of_term t with
 | Var id ->
diff --git a/toplevel/assumptions.mli b/toplevel/assumptions.mli
index 9c9f81bd2f..61beb26c8e 100644
--- a/toplevel/assumptions.mli
+++ b/toplevel/assumptions.mli
@@ -22,7 +22,7 @@ open Printer
 val traverse :
   Label.t -> constr ->
     (Refset_env.t * Refset_env.t Refmap_env.t *
-     (label * Context.rel_context * types) list Refmap_env.t)
+     (label * Context.Rel.t * types) list Refmap_env.t)
 
 (** Collects all the assumptions (optionally including opaque definitions)
    on which a term relies (together with their type). The above warning of
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 98686fb1b7..56106928e5 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -15,7 +15,6 @@ open Util
 open Pp
 open Term
 open Vars
-open Context
 open Termops
 open Declarations
 open Names
@@ -103,7 +102,7 @@ let mkFullInd (ind,u) n =
     context_chop (nparams-nparrec) mib.mind_params_ctxt in
   if nparrec > 0
     then mkApp (mkIndU (ind,u),
-      Array.of_list(extended_rel_list (nparrec+n) lnamesparrec))
+      Array.of_list(Context.Rel.to_extended_list (nparrec+n) lnamesparrec))
     else mkIndU (ind,u)
 
 let check_bool_is_defined () =
@@ -138,7 +137,7 @@ let build_beq_scheme mode kn =
         | Name s -> Id.of_string ("eq_"^(Id.to_string s))
         | Anonymous -> Id.of_string "eq_A"
     in
-    let ext_rel_list = extended_rel_list 0 lnamesparrec in
+    let ext_rel_list = Context.Rel.to_extended_list 0 lnamesparrec in
       let lift_cnt = ref 0 in
       let eqs_typ = List.map (fun aa ->
                                 let a = lift !lift_cnt aa in
@@ -234,7 +233,7 @@ let build_beq_scheme mode kn =
                Cn => match Y with ... end |]  part *)
     let ci = make_case_info env (fst ind) MatchStyle in
     let constrs n = get_constructors env (make_ind_family (ind,
-      extended_rel_list (n+nb_ind-1) mib.mind_params_ctxt)) in
+      Context.Rel.to_extended_list (n+nb_ind-1) mib.mind_params_ctxt)) in
     let constrsi = constrs (3+nparrec) in
     let n = Array.length constrsi in
     let ar = Array.make n (Lazy.force ff) in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 22baa5e61c..28a39b5706 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -12,7 +12,6 @@ open Pp
 open Names
 open Term
 open Vars
-open Context
 open Termops
 open Entries
 open Environ
@@ -198,13 +197,13 @@ let build_id_coercion idf_opt source poly =
   let val_f =
     it_mkLambda_or_LetIn
       (mkLambda (Name Namegen.default_dependent_ident,
-		 applistc vs (extended_rel_list 0 lams),
+		 applistc vs (Context.Rel.to_extended_list 0 lams),
 		 mkRel 1))
        lams
   in
   let typ_f =
     it_mkProd_wo_LetIn
-      (mkProd (Anonymous, applistc vs (extended_rel_list 0 lams), lift 1 t))
+      (mkProd (Anonymous, applistc vs (Context.Rel.to_extended_list 0 lams), lift 1 t))
       lams
   in
   (* juste pour verification *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 9cdb460644..ab18350c5c 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -351,7 +351,7 @@ let context poly l =
   let evars = ref (Evd.from_env env) in
   let _, ((env', fullctx), impls) = interp_context_evars env evars l in
   let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
-  let fullctx = Context.map_rel_context subst fullctx in
+  let fullctx = Context.Rel.map subst fullctx in
   let ce t = Evarutil.check_evars env Evd.empty !evars t in
   let () = List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx in
   let ctx =
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 2b7e9e4fe2..80ed246294 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Context
 open Environ
 open Constrexpr
 open Typeclasses
@@ -15,9 +14,9 @@ open Libnames
 
 (** Errors *)
 
-val mismatched_params : env -> constr_expr list -> rel_context -> 'a
+val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a
 
-val mismatched_props : env -> constr_expr list -> rel_context -> 'a
+val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
 
 (** Instance declaration *)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 91cfddb547..500769aca3 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -12,7 +12,6 @@ open Util
 open Flags
 open Term
 open Vars
-open Context
 open Termops
 open Entries
 open Environ
@@ -87,7 +86,7 @@ let interp_definition pl bl p red_option c ctypopt =
     match ctypopt with
       None ->
         let subst = evd_comb0 Evd.nf_univ_variables evdref in
-	let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in
+	let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
 	let env_bl = push_rel_context ctx env in
 	let c, imps2 = interp_constr_evars_impls ~impls env_bl evdref c in
         let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
@@ -100,7 +99,7 @@ let interp_definition pl bl p red_option c ctypopt =
     | Some ctyp ->
 	let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
 	let subst = evd_comb0 Evd.nf_univ_variables evdref in
-	let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in
+	let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
 	let env_bl = push_rel_context ctx env in
 	let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in
 	let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
@@ -125,7 +124,7 @@ let interp_definition pl bl p red_option c ctypopt =
 	  definition_entry ~types:typ ~poly:p 
 	    ~univs:uctx body
   in
-  red_constant_entry (rel_context_length ctx) ce !evdref red_option, !evdref, pl, imps
+  red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps
 
 let check_definition (ce, evd, _, imps) =
   check_evars_are_solved (Global.env ()) evd (Evd.empty,evd);
@@ -566,7 +565,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
 
   (* Compute interpretation metadatas *)
   let indimpls = List.map (fun (_, _, impls) -> userimpls @ 
-    lift_implicits (rel_context_nhyps ctx_params) impls) arities in
+    lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
   let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
   let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
   let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
@@ -592,11 +591,11 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
   let nf x = nf' (nf x) in
   let arities = List.map nf' arities in
   let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
-  let ctx_params = map_rel_context nf ctx_params in
+  let ctx_params = Context.Rel.map nf ctx_params in
   let evd = !evdref in
   let pl, uctx = Evd.universe_context ?names:pl evd in
   List.iter (check_evars env_params Evd.empty evd) arities;
-  iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;
+  Context.Rel.iter (check_evars env0 Evd.empty evd) ctx_params;
   List.iter (fun (_,ctyps,_) ->
     List.iter (check_evars env_ar_params Evd.empty evd) ctyps)
     constructors;
@@ -610,7 +609,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
     mind_entry_lc = ctypes
   }) indl arities aritypoly constructors in
   let impls =
-    let len = rel_context_nhyps ctx_params in
+    let len = Context.Rel.nhyps ctx_params in
       List.map2 (fun indimpls (_,_,cimpls) ->
 	indimpls, List.map (fun impls ->
 	  userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index b6da21e5ae..9416b7e7ad 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -9,7 +9,6 @@
 open Names
 open Errors
 open Util
-open Context
 open Term
 open Vars
 open Entries
@@ -37,8 +36,8 @@ let detype_param = function
 
 let abstract_inductive hyps nparams inds =
   let ntyp = List.length inds in
-  let nhyp = named_context_length hyps in
-  let args = instance_from_named_context (List.rev hyps) in
+  let nhyp = Context.Named.length hyps in
+  let args = Context.Named.to_instance (List.rev hyps) in
   let args = Array.of_list args in
   let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in
   let inds' =
@@ -100,7 +99,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
 	   Array.to_list mip.mind_consnames,
 	   Array.to_list lc))
       mib.mind_packets in
-  let sechyps' = map_named_context (expmod_constr modlist) sechyps in
+  let sechyps' = Context.Named.map (expmod_constr modlist) sechyps in
   let (params',inds') = abstract_inductive sechyps' nparams inds in
   let abs_ctx = Univ.instantiate_univ_context abs_ctx in
   let univs = Univ.UContext.union abs_ctx univs in
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index 386e4e3ef8..2984a0be82 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -6,10 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Context
 open Declarations
 open Entries
 open Opaqueproof
 
 val process_inductive :
-  named_context Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+  Context.Named.t Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index cac81a9395..e27e414377 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -13,7 +13,6 @@ open Declare
 *)
 
 open Term
-open Context
 open Vars
 open Names
 open Evd
@@ -44,7 +43,7 @@ let check_evars env evm =
 
 type oblinfo =
   { ev_name: int * Id.t;
-    ev_hyps: named_context;
+    ev_hyps: Context.Named.t;
     ev_status: Evar_kinds.obligation_definition_status;
     ev_chop: int option;
     ev_src: Evar_kinds.t Loc.located;
@@ -191,7 +190,7 @@ open Environ
 let eterm_obligations env name evm fs ?status t ty = 
   (* 'Serialize' the evars *)
   let nc = Environ.named_context env in
-  let nc_len = Context.named_context_length nc in
+  let nc_len = Context.Named.length nc in
   let evm = Evarutil.nf_evar_map_undefined evm in
   let evl = Evarutil.non_instantiated evm in
   let evl = Evar.Map.bindings evl in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 3a75004b08..12699b02b4 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -13,7 +13,6 @@ open Names
 open Globnames
 open Nameops
 open Term
-open Context
 open Vars
 open Environ
 open Declarations
@@ -148,8 +147,8 @@ let typecheck_params_and_fields def id pl t ps nots fs =
 	  else arity, evars
   in
   let evars, nf = Evarutil.nf_evars_and_universes evars in
-  let newps = map_rel_context nf newps in
-  let newfs = map_rel_context nf newfs in
+  let newps = Context.Rel.map nf newps in
+  let newfs = Context.Rel.map nf newfs in
   let ce t = Evarutil.check_evars env0 Evd.empty evars t in
     List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps);
     List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs);
@@ -244,8 +243,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
   let ctx = Univ.instantiate_univ_context mib.mind_universes in
   let indu = indsp, u in
   let r = mkIndU (indsp,u) in
-  let rp = applist (r, Context.extended_rel_list 0 paramdecls) in
-  let paramargs = Context.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
+  let rp = applist (r, Context.Rel.to_extended_list 0 paramdecls) in
+  let paramargs = Context.Rel.to_extended_list 1 paramdecls in (*def in [[params;x:rp]]*)
   let x = Name binder_name in
   let fields = instantiate_possibly_recursive_type indu paramdecls fields in
   let lifted_fields = Termops.lift_rel_context 1 fields in
@@ -353,7 +352,7 @@ open Typeclasses
 let declare_structure finite poly ctx id idbuild paramimpls params arity template 
     fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
   let nparams = List.length params and nfields = List.length fields in
-  let args = Context.extended_rel_list nfields params in
+  let args = Context.Rel.to_extended_list nfields params in
   let ind = applist (mkRel (1+nparams+nfields), args) in
   let type_constructor = it_mkProd_or_LetIn ind fields in
   let binder_name = 
diff --git a/toplevel/record.mli b/toplevel/record.mli
index eccb5d29d6..f68adcec8e 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Vernacexpr
 open Constrexpr
 open Impargs
@@ -22,15 +21,15 @@ val primitive_flag : bool ref
 
 val declare_projections :
   inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t ->
-  coercion_flag list -> manual_explicitation list list -> rel_context ->
+  coercion_flag list -> manual_explicitation list list -> Context.Rel.t ->
   (Name.t * bool) list * constant option list
 
 val declare_structure : Decl_kinds.recursivity_kind ->
   bool (** polymorphic?*) -> Univ.universe_context ->
   Id.t -> Id.t ->
-  manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *)
+  manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
   bool (** template arity ? *) ->
-  Impargs.manual_explicitation list list -> rel_context -> (** fields *)
+  Impargs.manual_explicitation list list -> Context.Rel.t -> (** fields *)
   ?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
   bool -> (** coercion? *)
   bool list -> (** field coercions *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 28b5bace13..2dacc04f09 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1580,7 +1580,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
                            (str "No such goal: " ++ int n ++ str "."))
       | _ , _ -> raise NoHyp in
     let hyps = pf_hyps gl in
-    let (id,bdyopt,typ) = Context.lookup_named id hyps in
+    let (id,bdyopt,typ) = Context.Named.lookup id hyps in
     let natureofid = match bdyopt with
       | None -> "Hypothesis"
       | Some bdy ->"Constant (let in)" in