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.

4 files changed, 62 insertions, 66 deletions

diff --git a/engine/evd.mli b/engine/evd.mli
index 57399f2b5..34169b021 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -10,7 +10,6 @@ open Util
 open Loc
 open Names
 open Term
-open Context
 open Environ
 
 (** {5 Existential variables and unification states}
@@ -105,8 +104,8 @@ type evar_info = {
 
 val make_evar : named_context_val -> types -> evar_info
 val evar_concl : evar_info -> constr
-val evar_context : evar_info -> named_context
-val evar_filtered_context : evar_info -> named_context
+val evar_context : evar_info -> Context.Named.t
+val evar_filtered_context : evar_info -> Context.Named.t
 val evar_hyps : evar_info -> named_context_val
 val evar_filtered_hyps : evar_info -> named_context_val
 val evar_body : evar_info -> evar_body
@@ -223,7 +222,7 @@ val existential_opt_value : evar_map -> existential -> constr option
 (** Same as {!existential_value} but returns an option instead of raising an
     exception. *)
 
-val evar_instance_array : (named_declaration -> 'a -> bool) -> evar_info ->
+val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info ->
   'a array -> (Id.t * 'a) list
 
 val instantiate_evar_array : evar_info -> constr -> constr array -> constr
@@ -423,7 +422,7 @@ val evar_list : constr -> existential list
 val evars_of_term : constr -> Evar.Set.t
   (** including evars in instances of evars *)
 
-val evars_of_named_context : named_context -> Evar.Set.t
+val evars_of_named_context : Context.Named.t -> Evar.Set.t
 
 val evars_of_filtered_evar_info : evar_info -> Evar.Set.t
 
diff --git a/engine/namegen.mli b/engine/namegen.mli
index f66bc6d88..617f6e522 100644
--- a/engine/namegen.mli
+++ b/engine/namegen.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Environ
 
 (*********************************************************************
@@ -39,13 +38,13 @@ val lambda_name : env -> Name.t * types * constr -> constr
 
 val prod_create : env -> types * types -> constr
 val lambda_create : env -> types * constr -> constr
-val name_assumption : env -> rel_declaration -> rel_declaration
-val name_context : env -> rel_context -> rel_context
+val name_assumption : env -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t
+val name_context : env -> Context.Rel.t -> Context.Rel.t
 
-val mkProd_or_LetIn_name : env -> types -> rel_declaration -> types
-val mkLambda_or_LetIn_name : env -> constr -> rel_declaration -> constr
-val it_mkProd_or_LetIn_name   : env -> types -> rel_context -> types
-val it_mkLambda_or_LetIn_name : env -> constr -> rel_context -> constr
+val mkProd_or_LetIn_name : env -> types -> Context.Rel.Declaration.t -> types
+val mkLambda_or_LetIn_name : env -> constr -> Context.Rel.Declaration.t -> constr
+val it_mkProd_or_LetIn_name   : env -> types -> Context.Rel.t -> types
+val it_mkLambda_or_LetIn_name : env -> constr -> Context.Rel.t -> constr
 
 (*********************************************************************
    Fresh names *)
diff --git a/engine/termops.ml b/engine/termops.ml
index c10c55220..ce640bacf 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -13,7 +13,6 @@ open Names
 open Nameops
 open Term
 open Vars
-open Context
 open Environ
 
 (* Sorts and sort family *)
@@ -700,9 +699,9 @@ let replace_term = replace_term_gen eq_constr
 
 let vars_of_env env =
   let s =
-    Context.fold_named_context (fun (id,_,_) s -> Id.Set.add id s)
+    Context.Named.fold_outside (fun (id,_,_) s -> Id.Set.add id s)
       (named_context env) ~init:Id.Set.empty in
-  Context.fold_rel_context
+  Context.Rel.fold_outside
     (fun (na,_,_) s -> match na with Name id -> Id.Set.add id s | _ -> s)
     (rel_context env) ~init:s
 
@@ -728,12 +727,12 @@ let lookup_rel_of_name id names =
 let empty_names_context = []
 
 let ids_of_rel_context sign =
-  Context.fold_rel_context
+  Context.Rel.fold_outside
     (fun (na,_,_) l -> match na with Name id -> id::l | Anonymous -> l)
     sign ~init:[]
 
 let ids_of_named_context sign =
-  Context.fold_named_context (fun (id,_,_) idl -> id::idl) sign ~init:[]
+  Context.Named.fold_outside (fun (id,_,_) idl -> id::idl) sign ~init:[]
 
 let ids_of_context env =
   (ids_of_rel_context (rel_context env))
@@ -788,7 +787,7 @@ let split_app c = match kind_of_term c with
 	c::(Array.to_list prev), last
   | _ -> assert false
 
-type subst = (rel_context*constr) Evar.Map.t
+type subst = (Context.Rel.t * constr) Evar.Map.t
 
 exception CannotFilter
 
@@ -825,7 +824,7 @@ let filtering env cv_pb c1 c2 =
   in
   aux env cv_pb c1 c2; !evm
 
-let decompose_prod_letin : constr -> int * rel_context * constr =
+let decompose_prod_letin : constr -> int * Context.Rel.t * constr =
   let rec prodec_rec i l c = match kind_of_term c with
     | Prod (n,t,c)    -> prodec_rec (succ i) ((n,None,t)::l) c
     | LetIn (n,d,t,c) -> prodec_rec (succ i) ((n,Some d,t)::l) c
@@ -861,7 +860,7 @@ let nb_prod_modulo_zeta x =
       | _ -> n
   in count 0 x
 
-let align_prod_letin c a : rel_context * constr =
+let align_prod_letin c a : Context.Rel.t * constr =
   let (lc,_,_) = decompose_prod_letin c in
   let (la,l,a) = decompose_prod_letin a in
   if not (la >= lc) then invalid_arg "align_prod_letin";
@@ -899,10 +898,10 @@ let process_rel_context f env =
   let sign = named_context_val env in
   let rels = rel_context env in
   let env0 = reset_with_named_context sign env in
-  Context.fold_rel_context f rels ~init:env0
+  Context.Rel.fold_outside f rels ~init:env0
 
 let assums_of_rel_context sign =
-  Context.fold_rel_context
+  Context.Rel.fold_outside
     (fun (na,c,t) l ->
       match c with
           Some _ -> l
@@ -912,7 +911,7 @@ let assums_of_rel_context sign =
 let map_rel_context_in_env f env sign =
   let rec aux env acc = function
     | d::sign ->
-	aux (push_rel d env) (map_rel_declaration (f env) d :: acc) sign
+	aux (push_rel d env) (Context.Rel.Declaration.map (f env) d :: acc) sign
     | [] ->
 	acc
   in
@@ -920,10 +919,10 @@ let map_rel_context_in_env f env sign =
 
 let map_rel_context_with_binders f sign =
   let rec aux k = function
-    | d::sign -> map_rel_declaration (f k) d :: aux (k-1) sign
+    | d::sign -> Context.Rel.Declaration.map (f k) d :: aux (k-1) sign
     | [] -> []
   in
-  aux (rel_context_length sign) sign
+  aux (Context.Rel.length sign) sign
 
 let substl_rel_context l =
   map_rel_context_with_binders (fun k -> substnl l (k-1))
@@ -955,7 +954,7 @@ let compact_named_context_reverse sign =
        if Option.equal Constr.equal c1 c2 && Constr.equal t1 t2
        then (i1::l2,c2,t2)::q
        else ([i1],c1,t1)::l
-  in Context.fold_named_context_reverse compact ~init:[] sign
+  in Context.Named.fold_inside compact ~init:[] sign
 
 let compact_named_context sign = List.rev (compact_named_context_reverse sign)
 
@@ -976,7 +975,7 @@ let global_vars_set_of_decl env = function
 let dependency_closure env sign hyps =
   if Id.Set.is_empty hyps then [] else
     let (_,lh) =
-      Context.fold_named_context_reverse
+      Context.Named.fold_inside
         (fun (hs,hl) (x,_,_ as d) ->
           if Id.Set.mem x hs then
             (Id.Set.union (global_vars_set_of_decl env d) (Id.Set.remove x hs),
diff --git a/engine/termops.mli b/engine/termops.mli
index 6083f1ab5..0fbd1ee82 100644
--- a/engine/termops.mli
+++ b/engine/termops.mli
@@ -9,7 +9,6 @@
 open Pp
 open Names
 open Term
-open Context
 open Environ
 
 (** printers *)
@@ -22,7 +21,7 @@ val set_print_constr : (env -> constr -> std_ppcmds) -> unit
 val print_constr     : constr -> std_ppcmds
 val print_constr_env : env -> constr -> std_ppcmds
 val print_named_context : env -> std_ppcmds
-val pr_rel_decl : env -> rel_declaration -> std_ppcmds
+val pr_rel_decl : env -> Context.Rel.Declaration.t -> std_ppcmds
 val print_rel_context : env -> std_ppcmds
 val print_env : env -> std_ppcmds
 
@@ -31,7 +30,7 @@ val push_rel_assum : Name.t * types -> env -> env
 val push_rels_assum : (Name.t * types) list -> env -> env
 val push_named_rec_types : Name.t array * types array * 'a -> env -> env
 
-val lookup_rel_id : Id.t -> rel_context -> int * constr option * types
+val lookup_rel_id : Id.t -> Context.Rel.t -> int * constr option * types
 (** Associates the contents of an identifier in a [rel_context]. Raise
     [Not_found] if there is no such identifier. *)
 
@@ -42,20 +41,20 @@ val rel_vect : int -> int -> constr array
 val rel_list : int -> int -> constr list
 
 (** iterators/destructors on terms *)
-val mkProd_or_LetIn : rel_declaration -> types -> types
-val mkProd_wo_LetIn : rel_declaration -> types -> types
+val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types
+val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types
 val it_mkProd : types -> (Name.t * types) list -> types
 val it_mkLambda : constr -> (Name.t * types) list -> constr
-val it_mkProd_or_LetIn : types -> rel_context -> types
-val it_mkProd_wo_LetIn : types -> rel_context -> types
-val it_mkLambda_or_LetIn : constr -> rel_context -> constr
-val it_mkNamedProd_or_LetIn : types -> named_context -> types
-val it_mkNamedProd_wo_LetIn : types -> named_context -> types
-val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr
+val it_mkProd_or_LetIn : types -> Context.Rel.t -> types
+val it_mkProd_wo_LetIn : types -> Context.Rel.t -> types
+val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr
+val it_mkNamedProd_or_LetIn : types -> Context.Named.t -> types
+val it_mkNamedProd_wo_LetIn : types -> Context.Named.t -> types
+val it_mkNamedLambda_or_LetIn : constr -> Context.Named.t -> constr
 
 (* Ad hoc version reinserting letin, assuming the body is defined in
    the context where the letins are expanded *)
-val it_mkLambda_or_LetIn_from_no_LetIn : constr -> rel_context -> constr
+val it_mkLambda_or_LetIn_from_no_LetIn : constr -> Context.Rel.t -> constr
 
 (** {6 Generic iterators on constr} *)
 
@@ -63,11 +62,11 @@ val map_constr_with_named_binders :
   (Name.t -> 'a -> 'a) ->
   ('a -> constr -> constr) -> 'a -> constr -> constr
 val map_constr_with_binders_left_to_right :
-  (rel_declaration -> 'a -> 'a) ->
+  (Context.Rel.Declaration.t -> 'a -> 'a) ->
   ('a -> constr -> constr) ->
     'a -> constr -> constr
 val map_constr_with_full_binders :
-  (rel_declaration -> 'a -> 'a) ->
+  (Context.Rel.Declaration.t -> 'a -> 'a) ->
   ('a -> constr -> constr) -> 'a -> constr -> constr
 
 (** [fold_constr_with_binders g f n acc c] folds [f n] on the immediate
@@ -81,11 +80,11 @@ val fold_constr_with_binders :
   ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b
 
 val fold_constr_with_full_binders :
-  (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
+  (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) ->
     'a -> 'b -> constr -> 'b
 
 val iter_constr_with_full_binders :
-  (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a ->
+  (Context.Rel.Declaration.t -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a ->
     constr -> unit
 
 (**********************************************************************)
@@ -110,7 +109,7 @@ val dependent : constr -> constr -> bool
 val dependent_no_evar : constr -> constr -> bool
 val dependent_univs : constr -> constr -> bool
 val dependent_univs_no_evar : constr -> constr -> bool
-val dependent_in_decl : constr -> named_declaration -> bool
+val dependent_in_decl : constr -> Context.Named.Declaration.t -> bool
 val count_occurrences : constr -> constr -> int
 val collect_metas : constr -> int list
 val collect_vars : constr -> Id.Set.t (** for visible vars only *)
@@ -164,11 +163,11 @@ exception CannotFilter
    (context,term), or raises [CannotFilter].
    Warning: Outer-kernel sort subtyping are taken into account: c1 has
    to be smaller than c2 wrt. sorts. *)
-type subst = (rel_context*constr) Evar.Map.t
-val filtering : rel_context -> Reduction.conv_pb -> constr -> constr -> subst
+type subst = (Context.Rel.t * constr) Evar.Map.t
+val filtering : Context.Rel.t -> Reduction.conv_pb -> constr -> constr -> subst
 
-val decompose_prod_letin : constr -> int * rel_context * constr
-val align_prod_letin : constr -> constr -> rel_context * constr
+val decompose_prod_letin : constr -> int * Context.Rel.t * constr
+val align_prod_letin : constr -> constr -> Context.Rel.t * constr
 
 (** [nb_lam] {% $ %}[x_1:T_1]...[x_n:T_n]c{% $ %} where {% $ %}c{% $ %} is not an abstraction
    gives {% $ %}n{% $ %} (casts are ignored) *)
@@ -197,51 +196,51 @@ val add_name : Name.t -> names_context -> names_context
 val lookup_name_of_rel : int -> names_context -> Name.t
 val lookup_rel_of_name : Id.t -> names_context -> int
 val empty_names_context : names_context
-val ids_of_rel_context : rel_context -> Id.t list
-val ids_of_named_context : named_context -> Id.t list
+val ids_of_rel_context : Context.Rel.t -> Id.t list
+val ids_of_named_context : Context.Named.t -> Id.t list
 val ids_of_context : env -> Id.t list
 val names_of_rel_context : env -> names_context
 
 (* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has
    [n] hypotheses, excluding local definitions, and [Γ₁], if not empty,
    starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *)
-val context_chop : int -> rel_context -> rel_context * rel_context
+val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t
 
 (* [env_rel_context_chop n env] extracts out the [n] top declarations
    of the rel_context part of [env], counting both local definitions and
    hypotheses *)
-val env_rel_context_chop : int -> env -> env * rel_context
+val env_rel_context_chop : int -> env -> env * Context.Rel.t
 
 (** Set of local names *)
 val vars_of_env: env -> Id.Set.t
 val add_vname : Id.Set.t -> Name.t -> Id.Set.t
 
 (** other signature iterators *)
-val process_rel_context : (rel_declaration -> env -> env) -> env -> env
-val assums_of_rel_context : rel_context -> (Name.t * constr) list
-val lift_rel_context : int -> rel_context -> rel_context
-val substl_rel_context : constr list -> rel_context -> rel_context
-val smash_rel_context : rel_context -> rel_context (** expand lets in context *)
+val process_rel_context : (Context.Rel.Declaration.t -> env -> env) -> env -> env
+val assums_of_rel_context : Context.Rel.t -> (Name.t * constr) list
+val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t
+val substl_rel_context : constr list -> Context.Rel.t -> Context.Rel.t
+val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *)
 
 val map_rel_context_in_env :
-  (env -> constr -> constr) -> env -> rel_context -> rel_context
+  (env -> constr -> constr) -> env -> Context.Rel.t -> Context.Rel.t
 val map_rel_context_with_binders :
-  (int -> constr -> constr) -> rel_context -> rel_context
+  (int -> constr -> constr) -> Context.Rel.t -> Context.Rel.t
 val fold_named_context_both_sides :
-  ('a -> named_declaration -> named_declaration list -> 'a) ->
-    named_context -> init:'a -> 'a
-val mem_named_context : Id.t -> named_context -> bool
-val compact_named_context : named_context -> named_list_context
-val compact_named_context_reverse : named_context -> named_list_context
+  ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) ->
+    Context.Named.t -> init:'a -> 'a
+val mem_named_context : Id.t -> Context.Named.t -> bool
+val compact_named_context : Context.Named.t -> Context.NamedList.t
+val compact_named_context_reverse : Context.Named.t -> Context.NamedList.t
 
 val clear_named_body : Id.t -> env -> env
 
 val global_vars : env -> constr -> Id.t list
-val global_vars_set_of_decl : env -> named_declaration -> Id.Set.t
+val global_vars_set_of_decl : env -> Context.Named.Declaration.t -> Id.Set.t
 
 (** Gives an ordered list of hypotheses, closed by dependencies,
    containing a given set *)
-val dependency_closure : env -> named_context -> Id.Set.t -> Id.t list
+val dependency_closure : env -> Context.Named.t -> Id.Set.t -> Id.t list
 
 (** Test if an identifier is the basename of a global reference *)
 val is_section_variable : Id.t -> bool