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.

3 files changed, 12 insertions, 14 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 2e112f9ac..773127c77 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -293,7 +293,7 @@ let pr_named_context_of env sigma =
   hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl)
 
 let pr_named_context env sigma ne_context =
-  hv 0 (Context.fold_named_context
+  hv 0 (Context.Named.fold_outside
 	  (fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d)
           ne_context ~init:(mt ()))
 
@@ -306,7 +306,7 @@ let pr_rel_context_of env sigma =
 (* Prints an env (variables and de Bruijn). Separator: newline *)
 let pr_context_unlimited env sigma =
   let sign_env =
-    Context.fold_named_list_context
+    Context.NamedList.fold
       (fun d pps ->
          let pidt =  pr_var_list_decl env sigma d in
          (pps ++ fnl () ++ pidt))
@@ -333,7 +333,7 @@ let pr_context_limit n env sigma =
   else
     let k = lgsign-n in
     let _,sign_env =
-      Context.fold_named_list_context
+      Context.NamedList.fold
         (fun d (i,pps) ->
            if i < k then
 	     (i+1, (pps ++str "."))
@@ -726,7 +726,7 @@ let prterm = pr_lconstr
 
 type context_object =
   | Variable of Id.t (* A section variable or a Let definition *)
-  | Axiom of constant * (Label.t * Context.rel_context * types) list
+  | Axiom of constant * (Label.t * Context.Rel.t * types) list
   | Opaque of constant     (* An opaque constant. *)
   | Transparent of constant
 
diff --git a/printing/printer.mli b/printing/printer.mli
index 5c60b8936..bdb295a47 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -10,7 +10,6 @@ open Pp
 open Names
 open Globnames
 open Term
-open Context
 open Environ
 open Pattern
 open Evd
@@ -109,13 +108,13 @@ val pr_pconstructor        : env -> pconstructor -> std_ppcmds
 val pr_context_unlimited   : env -> evar_map -> std_ppcmds
 val pr_ne_context_of       : std_ppcmds -> env -> evar_map -> std_ppcmds
 
-val pr_var_decl            : env -> evar_map -> named_declaration -> std_ppcmds
-val pr_var_list_decl       : env -> evar_map -> named_list_declaration -> std_ppcmds
-val pr_rel_decl            : env -> evar_map -> rel_declaration -> std_ppcmds
+val pr_var_decl            : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds
+val pr_var_list_decl       : env -> evar_map -> Context.NamedList.Declaration.t -> std_ppcmds
+val pr_rel_decl            : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds
 
-val pr_named_context       : env -> evar_map -> named_context -> std_ppcmds
+val pr_named_context       : env -> evar_map -> Context.Named.t -> std_ppcmds
 val pr_named_context_of    : env -> evar_map -> std_ppcmds
-val pr_rel_context         : env -> evar_map -> rel_context -> std_ppcmds
+val pr_rel_context         : env -> evar_map -> Context.Rel.t -> std_ppcmds
 val pr_rel_context_of      : env -> evar_map -> std_ppcmds
 val pr_context_of          : env -> evar_map -> std_ppcmds
 
@@ -165,7 +164,7 @@ val prterm                 : constr -> std_ppcmds (** = pr_lconstr *)
 type context_object =
   | Variable of Id.t  (** A section variable or a Let definition *)
   (** An axiom and the type it inhabits (if an axiom of the empty type) *)
-  | Axiom of constant * (Label.t * Context.rel_context * types) list
+  | Axiom of constant * (Label.t * Context.Rel.t * types) list
   | Opaque of constant      (** An opaque constant. *)
   | Transparent of constant (** A transparent constant *)
 
diff --git a/printing/printmod.ml b/printing/printmod.ml
index d6f847cc7..d277d3782 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -65,7 +65,6 @@ let get_new_id locals id =
 
 (** Inductive declarations *)
 
-open Context
 open Termops
 open Reduction
 
@@ -90,7 +89,7 @@ let print_one_inductive env sigma mib ((_,i) as ind) =
     else Univ.Instance.empty in
   let mip = mib.mind_packets.(i) in
   let params = Inductive.inductive_paramdecls (mib,u) in
-  let args = extended_rel_list 0 params in
+  let args = Context.Rel.to_extended_list 0 params in
   let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors (ind,u) (mib,mip) in
   let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in
@@ -144,7 +143,7 @@ let print_record env mind mib =
   in
   let mip = mib.mind_packets.(0) in
   let params = Inductive.inductive_paramdecls (mib,u) in
-  let args = extended_rel_list 0 params in
+  let args = Context.Rel.to_extended_list 0 params in
   let arity = hnf_prod_applist env (build_ind_type env ((mib,mip),u)) args in
   let cstrtypes = Inductive.type_of_constructors ((mind,0),u) (mib,mip) in
   let cstrtype = hnf_prod_applist env cstrtypes.(0) args in