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.

6 files changed, 13 insertions, 18 deletions

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 2dc2420c4..923743ece 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -11,7 +11,6 @@ open Util
 open Names
 open Term
 open Vars
-open Context
 open Declarations
 open Declareops
 open Environ
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 6c7b09383..d306112ce 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Term
-open Context
 open Globnames
 
 val qflag : bool ref
@@ -27,7 +26,7 @@ type counter = bool -> metavariable
 val construct_nhyps : pinductive -> Proof_type.goal Tacmach.sigma -> int array
 
 val ind_hyps : int -> pinductive -> constr list ->
-  Proof_type.goal Tacmach.sigma -> rel_context array
+  Proof_type.goal Tacmach.sigma -> Context.Rel.t array
 
 type atoms = {positive:constr list;negative:constr list}
 
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f57f12f66..ad18ea95a 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -3,7 +3,6 @@ open Errors
 open Util
 open Term
 open Vars
-open Context
 open Namegen
 open Names
 open Declarations
@@ -230,7 +229,7 @@ let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta
 
 
 
-let change_eq env sigma hyp_id (context:rel_context) x t end_of_type  =
+let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
   let nochange ?t' msg  =
     begin
       observe (str ("Not treating ( "^msg^" )") ++ pr_lconstr t  ++ str "    " ++ match t' with None -> str "" | Some t -> Printer.pr_lconstr t );
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index bbe2f1a3a..e2c3bbb97 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -3,7 +3,6 @@ open Errors
 open Util
 open Term
 open Vars
-open Context
 open Namegen
 open Names
 open Pp
@@ -30,7 +29,7 @@ let compute_new_princ_type_from_rel rel_to_fun sorts princ_type =
   let env = Global.env () in
   let env_with_params = Environ.push_rel_context princ_type_info.params env in
   let tbl = Hashtbl.create 792 in
-  let rec change_predicates_names (avoid:Id.t list) (predicates:rel_context)  : rel_context =
+  let rec change_predicates_names (avoid:Id.t list) (predicates:Context.Rel.t)  : Context.Rel.t =
     match predicates with
     | [] -> []
     |(Name x,v,t)::predicates ->
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 5d92fca5e..80de8e764 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -357,7 +357,7 @@ let add_pat_variables pat typ env : Environ.env =
   let new_env = add_pat_variables  env pat typ in
   let res =
     fst (
-      Context.fold_rel_context
+      Context.Rel.fold_outside
 	(fun (na,v,t) (env,ctxt) ->
 	 match na with
 	   | Anonymous -> assert false
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index e3455e770..be04728e0 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -19,7 +19,6 @@ open Pp
 open Names
 open Term
 open Vars
-open Context
 open Termops
 open Declarations
 open Glob_term
@@ -258,27 +257,27 @@ type merge_infos =
       lnk2: int merged_arg array;
 
       (** rec params which remain rec param (ie not linked) *)
-      recprms1: rel_declaration list;
-      recprms2: rel_declaration list;
+      recprms1: Context.Rel.Declaration.t list;
+      recprms2: Context.Rel.Declaration.t list;
       nrecprms1: int;
       nrecprms2: int;
 
       (** rec parms which became non parm (either linked to something
          or because after a rec parm that became non parm) *)
-      otherprms1: rel_declaration list;
-      otherprms2: rel_declaration list;
+      otherprms1: Context.Rel.Declaration.t list;
+      otherprms2: Context.Rel.Declaration.t list;
       notherprms1:int;
       notherprms2:int;
 
       (** args which remain args in merge *)
-      args1:rel_declaration list;
-      args2:rel_declaration list;
+      args1:Context.Rel.Declaration.t list;
+      args2:Context.Rel.Declaration.t list;
       nargs1:int;
       nargs2:int;
 
       (** functional result args *)
-      funresprms1: rel_declaration list;
-      funresprms2: rel_declaration list;
+      funresprms1: Context.Rel.Declaration.t list;
+      funresprms2: Context.Rel.Declaration.t list;
       nfunresprms1:int;
       nfunresprms2:int;
     }
@@ -851,7 +850,7 @@ let glob_constr_list_to_inductive_expr prms1 prms2 mib1 mib2 shift
   lident , bindlist , Some cstr_expr , lcstor_expr
 
 
-let mkProd_reldecl (rdecl:rel_declaration) (t2:glob_constr) =
+let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
   match rdecl with
     | (nme,None,t) ->
         let traw = Detyping.detype false [] (Global.env()) Evd.empty t in