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.

1 files changed, 18 insertions, 19 deletions

diff --git a/kernel/term.mli b/kernel/term.mli
index 972a67ebe..c45e04338 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -7,7 +7,6 @@
 (************************************************************************)
 
 open Names
-open Context
 
 (** {5 Redeclaration of types from module Constr and Sorts}
 
@@ -213,14 +212,14 @@ val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr
 val mkNamedProd : Id.t -> types -> types -> types
 
 (** Constructs either [(x:t)c] or [[x=b:t]c] *)
-val mkProd_or_LetIn : rel_declaration -> types -> types
-val mkProd_wo_LetIn : rel_declaration -> types -> types
-val mkNamedProd_or_LetIn : named_declaration -> types -> types
-val mkNamedProd_wo_LetIn : named_declaration -> types -> types
+val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
+val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types
+val mkNamedProd_or_LetIn : Context.Named.Declaration.t -> types -> types
+val mkNamedProd_wo_LetIn : Context.Named.Declaration.t -> types -> types
 
 (** Constructs either [[x:t]c] or [[x=b:t]c] *)
-val mkLambda_or_LetIn : rel_declaration -> constr -> constr
-val mkNamedLambda_or_LetIn : named_declaration -> constr -> constr
+val mkLambda_or_LetIn : Context.Rel.Declaration.t -> constr -> constr
+val mkNamedLambda_or_LetIn : Context.Named.Declaration.t -> constr -> constr
 
 (** {5 Other term constructors. } *)
 
@@ -262,8 +261,8 @@ val to_lambda : int -> constr -> constr
    where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *)
 val to_prod : int -> constr -> constr
 
-val it_mkLambda_or_LetIn : constr -> rel_context -> constr
-val it_mkProd_or_LetIn : types -> rel_context -> types
+val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
+val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
 
 (** In [lambda_applist c args], [c] is supposed to have the form
     [λΓ.c] with [Γ] without let-in; it returns [c] with the variables
@@ -314,29 +313,29 @@ val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr
 
 (** Extract the premisses and the conclusion of a term of the form
    "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *)
-val decompose_prod_assum : types -> rel_context * types
+val decompose_prod_assum : types -> Context.Rel.t * types
 
 (** Idem with lambda's *)
-val decompose_lam_assum : constr -> rel_context * constr
+val decompose_lam_assum : constr -> Context.Rel.t * constr
 
 (** Idem but extract the first [n] premisses, counting let-ins. *)
-val decompose_prod_n_assum : int -> types -> rel_context * types
+val decompose_prod_n_assum : int -> types -> Context.Rel.t * types
 
 (** Idem for lambdas, _not_ counting let-ins *)
-val decompose_lam_n_assum : int -> constr -> rel_context * constr
+val decompose_lam_n_assum : int -> constr -> Context.Rel.t * constr
 
 (** Idem, counting let-ins *)
-val decompose_lam_n_decls : int -> constr -> rel_context * constr
+val decompose_lam_n_decls : int -> constr -> Context.Rel.t * constr
 
 (** Return the premisses/parameters of a type/term (let-in included) *)
-val prod_assum : types -> rel_context
-val lam_assum : constr -> rel_context
+val prod_assum : types -> Context.Rel.t
+val lam_assum : constr -> Context.Rel.t
 
 (** Return the first n-th premisses/parameters of a type (let included and counted) *)
-val prod_n_assum : int -> types -> rel_context
+val prod_n_assum : int -> types -> Context.Rel.t
 
 (** Return the first n-th premisses/parameters of a term (let included but not counted) *)
-val lam_n_assum : int -> constr -> rel_context
+val lam_n_assum : int -> constr -> Context.Rel.t
 
 (** Remove the premisses/parameters of a type/term *)
 val strip_prod : types -> types
@@ -369,7 +368,7 @@ val under_outer_cast : (constr -> constr) -> constr -> constr
     Such a term can canonically be seen as the pair of a context of types
     and of a sort *)
 
-type arity = rel_context * sorts
+type arity = Context.Rel.t * sorts
 
 (** Build an "arity" from its canonical form *)
 val mkArity : arity -> types