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, 22 insertions, 23 deletions

diff --git a/kernel/environ.mli b/kernel/environ.mli
index 2eab32e72..f3fe4d6ae 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Declarations
 open Univ
 
@@ -42,8 +41,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool
 val empty_env : env
 
 val universes     : env -> UGraph.t
-val rel_context   : env -> rel_context
-val named_context : env -> named_context
+val rel_context   : env -> Context.Rel.t
+val named_context : env -> Context.Named.t
 val named_context_val : env -> named_context_val
 
 val opaque_tables : env -> Opaqueproof.opaquetab
@@ -60,25 +59,25 @@ val empty_context : env -> bool
 (** {5 Context of de Bruijn variables ([rel_context]) } *)
 
 val nb_rel           : env -> int
-val push_rel         : rel_declaration -> env -> env
-val push_rel_context :     rel_context -> env -> env
+val push_rel         : Context.Rel.Declaration.t -> env -> env
+val push_rel_context : Context.Rel.t -> env -> env
 val push_rec_types   : rec_declaration -> env -> env
 
 (** Looks up in the context of local vars referred by indice ([rel_context]) 
    raises [Not_found] if the index points out of the context *)
-val lookup_rel    : int -> env -> rel_declaration
+val lookup_rel    : int -> env -> Context.Rel.Declaration.t
 val evaluable_rel : int -> env -> bool
 
 (** {6 Recurrence on [rel_context] } *)
 
 val fold_rel_context :
-  (env -> rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
+  (env -> Context.Rel.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a
 
 (** {5 Context of variables (section variables and goal assumptions) } *)
 
-val named_context_of_val : named_context_val -> named_context
+val named_context_of_val : named_context_val -> Context.Named.t
 val named_vals_of_val : named_context_val -> Pre_env.named_vals
-val val_of_named_context : named_context -> named_context_val
+val val_of_named_context : Context.Named.t -> named_context_val
 val empty_named_context_val : named_context_val
 
 
@@ -88,18 +87,18 @@ val empty_named_context_val : named_context_val
 val map_named_val :
    (constr -> constr) -> named_context_val -> named_context_val
 
-val push_named : named_declaration -> env -> env
-val push_named_context : named_context -> env -> env
+val push_named : Context.Named.Declaration.t -> env -> env
+val push_named_context : Context.Named.t -> env -> env
 val push_named_context_val  :
-    named_declaration -> named_context_val -> named_context_val
+    Context.Named.Declaration.t -> named_context_val -> named_context_val
 
 
 
 (** Looks up in the context of local vars referred by names ([named_context]) 
    raises [Not_found] if the Id.t is not found *)
 
-val lookup_named     : variable -> env -> named_declaration
-val lookup_named_val : variable -> named_context_val -> named_declaration
+val lookup_named     : variable -> env -> Context.Named.Declaration.t
+val lookup_named_val : variable -> named_context_val -> Context.Named.Declaration.t
 val evaluable_named  : variable -> env -> bool
 val named_type : variable -> env -> types
 val named_body : variable -> env -> constr option
@@ -107,11 +106,11 @@ val named_body : variable -> env -> constr option
 (** {6 Recurrence on [named_context]: older declarations processed first } *)
 
 val fold_named_context :
-  (env -> named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
+  (env -> Context.Named.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a
 
 (** Recurrence on [named_context] starting from younger decl *)
 val fold_named_context_reverse :
-  ('a -> named_declaration -> 'a) -> init:'a -> env -> 'a
+  ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a
 
 (** This forgets named and rel contexts *)
 val reset_context : env -> env
@@ -228,7 +227,7 @@ val vars_of_global : env -> constr -> Id.Set.t
 val really_needed : env -> Id.Set.t -> Id.Set.t
 
 (** like [really_needed] but computes a well ordered named context *)
-val keep_hyps : env -> Id.Set.t -> section_context
+val keep_hyps : env -> Id.Set.t -> Context.section_context
 
 (** {5 Unsafe judgments. }
     We introduce here the pre-type of judgments, which is
@@ -258,22 +257,22 @@ exception Hyp_not_found
    return [tail::(f head (id,_,_) (rev tail))::head].
    the value associated to id should not change *)
 val apply_to_hyp : named_context_val -> variable ->
-  (named_context -> named_declaration -> named_context -> named_declaration) ->
+  (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) ->
     named_context_val
 
 (** [apply_to_hyp_and_dependent_on sign id f g] split [sign] into
    [tail::(id,_,_)::head] and
    return [(g tail)::(f (id,_,_))::head]. *)
 val apply_to_hyp_and_dependent_on : named_context_val -> variable ->
-  (named_declaration -> named_context_val -> named_declaration) ->
-    (named_declaration -> named_context_val -> named_declaration) ->
+  (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) ->
+    (Context.Named.Declaration.t -> named_context_val -> Context.Named.Declaration.t) ->
       named_context_val
 
 val insert_after_hyp : named_context_val -> variable ->
-  named_declaration ->
-    (named_context -> unit) -> named_context_val
+  Context.Named.Declaration.t ->
+    (Context.Named.t -> unit) -> named_context_val
 
-val remove_hyps : Id.Set.t -> (named_declaration -> named_declaration) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val
+val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (Pre_env.lazy_val -> Pre_env.lazy_val) -> named_context_val -> named_context_val