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, 16 insertions, 17 deletions

diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 11df40caf..da2d213ff 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -12,7 +12,6 @@ open Names
 open Univ
 open Term
 open Vars
-open Context
 open Declarations
 open Declareops
 open Inductive
@@ -341,7 +340,7 @@ let typecheck_inductive env mie =
 type ill_formed_ind =
   | LocalNonPos of int
   | LocalNotEnoughArgs of int
-  | LocalNotConstructor of rel_context * constr list
+  | LocalNotConstructor of Context.Rel.t * constr list
   | LocalNonPar of int * int * int
 
 exception IllFormedInd of ill_formed_ind
@@ -361,7 +360,7 @@ let explain_ind_err id ntyp env nbpar c err =
 	raise (InductiveError
 		 (NotEnoughArgs (env,c',mkRel (kt+nbpar))))
     | LocalNotConstructor (paramsctxt,args)->
-        let nparams = rel_context_nhyps paramsctxt in
+        let nparams = Context.Rel.nhyps paramsctxt in
 	raise (InductiveError
 		 (NotConstructor (env,id,c',mkRel (ntyp+nbpar),nparams,
                                   List.length args - nparams)))
@@ -384,7 +383,7 @@ let failwith_non_pos_list n ntypes l =
 
 (* Check the inductive type is called with the expected parameters *)
 let check_correct_par (env,n,ntypes,_) hyps l largs =
-  let nparams = rel_context_nhyps hyps in
+  let nparams = Context.Rel.nhyps hyps in
   let largs = Array.of_list largs in
   if Array.length largs < nparams then
     raise (IllFormedInd (LocalNotEnoughArgs l));
@@ -465,8 +464,8 @@ let array_min nmr a = if Int.equal nmr 0 then 0 else
     arguments (used to generate induction schemes, so a priori less
     relevant to the kernel). *)
 let check_positivity_one (env,_,ntypes,_ as ienv) hyps (_,i as ind) nargs lcnames indlc =
-  let lparams = rel_context_length hyps in
-  let nmr = rel_context_nhyps hyps in
+  let lparams = Context.Rel.length hyps in
+  let nmr = Context.Rel.nhyps hyps in
   (** Positivity of one argument [c] of a constructor (i.e. the
       constructor [cn] has a type of the shape [… -> c … -> P], where,
       more generally, the arrows may be dependent). *)
@@ -617,13 +616,13 @@ let check_positivity kn env_ar params inds =
   let ntypes = Array.length inds in
   let rc = Array.mapi (fun j t -> (Mrec (kn,j),t)) (Rtree.mk_rec_calls ntypes) in
   let lra_ind = Array.rev_to_list rc in
-  let lparams = rel_context_length params in
-  let nmr = rel_context_nhyps params in
+  let lparams = Context.Rel.length params in
+  let nmr = Context.Rel.nhyps params in
   let check_one i (_,lcnames,lc,(sign,_)) =
     let ra_env =
       List.init lparams (fun _ -> (Norec,mk_norec)) @ lra_ind in
     let ienv = (env_ar, 1+lparams, ntypes, ra_env) in
-    let nargs = rel_context_nhyps sign - nmr in
+    let nargs = Context.Rel.nhyps sign - nmr in
     check_positivity_one ienv params (kn,i) nargs lcnames lc
   in
   let irecargs_nmr = Array.mapi check_one inds in
@@ -697,7 +696,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
       matching with a parameter context. *)
   let indty, paramsletsubst =
     (* [ty] = [Ind inst] is typed in context [params] *)
-    let inst = extended_rel_vect 0 paramslet in
+    let inst = Context.Rel.to_extended_vect 0 paramslet in
     let ty = mkApp (mkIndU indu, inst) in
     (* [Ind inst] is typed in context [params-wo-let] *)
     let inst' = rel_list 0 nparamargs in
@@ -710,7 +709,7 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
   in
   let ci = 
     let print_info =
-      { ind_tags = []; cstr_tags = [|rel_context_tags ctx|]; style = LetStyle } in
+      { ind_tags = []; cstr_tags = [|Context.Rel.to_tags ctx|]; style = LetStyle } in
       { ci_ind     = ind;
 	ci_npar    = nparamargs;
 	ci_cstr_ndecls = mind_consnrealdecls;
@@ -783,8 +782,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
   let ntypes = Array.length inds in
   (* Compute the set of used section variables *)
   let hyps = used_section_variables env inds in
-  let nparamargs = rel_context_nhyps params in
-  let nparamdecls = rel_context_length params in
+  let nparamargs = Context.Rel.nhyps params in
+  let nparamdecls = Context.Rel.length params in
   let subst, ctx = Univ.abstract_universes p ctx in
   let params = Vars.subst_univs_level_context subst params in
   let env_ar = 
@@ -799,10 +798,10 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
     let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
     let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
     let consnrealdecls =
-      Array.map (fun (d,_) -> rel_context_length d - rel_context_length params)
+      Array.map (fun (d,_) -> Context.Rel.length d - Context.Rel.length params)
 	splayed_lc in
     let consnrealargs =
-      Array.map (fun (d,_) -> rel_context_nhyps d - rel_context_nhyps params)
+      Array.map (fun (d,_) -> Context.Rel.nhyps d - Context.Rel.nhyps params)
 	splayed_lc in
     (* Elimination sorts *)
     let arkind,kelim = 
@@ -835,8 +834,8 @@ let build_inductive env p prv ctx env_ar params kn isrecord isfinite inds nmr re
       { mind_typename = id;
 	mind_arity = arkind;
 	mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign;
-	mind_nrealargs = rel_context_nhyps ar_sign - nparamargs;
-	mind_nrealdecls = rel_context_length ar_sign - nparamdecls;
+	mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs;
+	mind_nrealdecls = Context.Rel.length ar_sign - nparamdecls;
 	mind_kelim = kelim;
 	mind_consnames = Array.of_list cnames;
 	mind_consnrealdecls = consnrealdecls;