CLEANUP: minor readability improvements

mainly concerning referring to "Context.{Rel,Named}.get_{id,value,type}" functions.

If multiple modules define a function with a same name, e.g.:

	Context.{Rel,Named}.get_type

those calls were prefixed with a corresponding prefix
to make sure that it is obvious which function is being called.

11 files changed, 50 insertions, 42 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 134599150..db09e5ed7 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -21,6 +21,8 @@ open Declarations
 open Environ
 open Univ
 
+module NamedDecl = Context.Named.Declaration
+
 (*s Cooking the constants. *)
 
 let pop_dirpath p = match DirPath.repr p with
@@ -202,8 +204,7 @@ let cook_constant env { from = cb; info } =
   in
   let const_hyps =
     Context.Named.fold_outside (fun decl hyps ->
-      let open Context.Named.Declaration in
-      List.filter (fun decl' -> not (Id.equal (get_id decl) (get_id decl')))
+      List.filter (fun decl' -> not (Id.equal (NamedDecl.get_id decl) (NamedDecl.get_id decl')))
 		  hyps)
       hyps ~init:cb.const_hyps in
   let typ = match cb.const_type with
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index acd73d97d..3177b5fae 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -22,6 +22,8 @@ open Declarations
 open Pre_env
 open Cbytegen
 
+module NamedDecl = Context.Named.Declaration
+module RelDecl = Context.Rel.Declaration
 
 external tcode_of_code : emitcodes -> int -> tcode = "coq_tcode_of_code"
 external eval_tcode : tcode -> values array -> values = "coq_eval_tcode"
@@ -189,18 +191,14 @@ and slot_for_fv env fv =
       let nv = Pre_env.lookup_named_val id env in
       begin match force_lazy_val nv with
       | None ->
-         let open Context.Named in
-         let open Declaration in
-	 env.env_named_context |> lookup id |> get_value |> fill_fv_cache nv id val_of_named idfun
+	 env.env_named_context |> Context.Named.lookup id |> NamedDecl.get_value |> fill_fv_cache nv id val_of_named idfun
       | Some (v, _) -> v
       end
   | FVrel i ->
       let rv = Pre_env.lookup_rel_val i env in
       begin match force_lazy_val rv with
       | None ->
-         let open Context.Rel in
-         let open Declaration in
-	 env.env_rel_context |> lookup i |> get_value |> fill_fv_cache rv i val_of_rel env_of_rel
+	 env.env_rel_context |> Context.Rel.lookup i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel
       | Some (v, _) -> v
       end
   | FVuniv_var idu ->
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 211e5e062..8943de404 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -9,7 +9,8 @@
 open Declarations
 open Mod_subst
 open Util
-open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
 
 (** Operations concernings types in [Declarations] :
     [constant_body], [mutual_inductive_body], [module_body] ... *)
@@ -94,7 +95,7 @@ let is_opaque cb = match cb.const_body with
 (** {7 Constant substitutions } *)
 
 let subst_rel_declaration sub =
-  map_constr (subst_mps sub)
+  RelDecl.map_constr (subst_mps sub)
 
 let subst_rel_context sub = List.smartmap (subst_rel_declaration sub)
 
@@ -146,7 +147,7 @@ let subst_const_body sub cb =
     themselves. But would it really bring substantial gains ? *)
 
 let hcons_rel_decl =
-  map_type Term.hcons_types % map_value Term.hcons_constr % map_name Names.Name.hcons
+  RelDecl.map_type Term.hcons_types % RelDecl.map_value Term.hcons_constr % RelDecl.map_name Names.Name.hcons
 
 let hcons_rel_context l = List.smartmap hcons_rel_decl l
 
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index bd91c689d..dce4e9307 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -18,6 +18,9 @@ open Reduction
 open Inductive
 open Type_errors
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
 let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y
 
 let conv_leq_vecti env v1 v2 =
@@ -73,8 +76,7 @@ let judge_of_type u =
 
 let judge_of_relative env n =
   try
-    let open Context.Rel.Declaration in
-    env |> lookup_rel n |> get_type |> lift n
+    env |> lookup_rel n |> RelDecl.get_type |> lift n
   with Not_found ->
     error_unbound_rel env n
 
@@ -92,9 +94,8 @@ let judge_of_variable env id =
 let check_hyps_inclusion env f c sign =
   Context.Named.fold_outside
     (fun decl () ->
-      let open Context.Named.Declaration in
-      let id = get_id decl in
-      let ty1 = get_type decl in
+      let id = NamedDecl.get_id decl in
+      let ty1 = NamedDecl.get_type decl in
       try
         let ty2 = named_type id env in
         if not (eq_constr ty2 ty1) then raise Exit
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index e2f43b93e..3864df6c9 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1832,10 +1832,9 @@ and apply_fv env sigma univ (fv_named,fv_rel) auxdefs ml =
   auxdefs, MLlet(aux_name, ml, mkMLapp (MLlocal aux_name) (Array.of_list (fv_rel@fv_named)))
 
 and compile_rel env sigma univ auxdefs n =
-  let open Context.Rel in
-  let n = length env.env_rel_context - n in
-  let open Declaration in
-  match lookup n env.env_rel_context with
+  let n = Context.Rel.length env.env_rel_context - n in
+  let open Context.Rel.Declaration in
+  match Context.Rel.lookup n env.env_rel_context with
   | LocalDef (_,t,_) ->
       let code = lambda_of_constr env sigma t in
       let auxdefs,code = compile_with_fv env sigma univ auxdefs None code in
diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml
index 91b40be7e..366f9a0a6 100644
--- a/kernel/nativelambda.ml
+++ b/kernel/nativelambda.ml
@@ -14,6 +14,8 @@ open Pre_env
 open Nativevalues
 open Nativeinstr
 
+module RelDecl = Context.Rel.Declaration
+
 (** This file defines the lambda code generation phase of the native compiler *)
 
 exception NotClosed
@@ -727,8 +729,7 @@ let optimize lam =
 let lambda_of_constr env sigma c =
   set_global_env env;
   let env = Renv.make () in
-  let open Context.Rel.Declaration in
-  let ids = List.rev_map get_name !global_env.env_rel_context in
+  let ids = List.rev_map RelDecl.get_name !global_env.env_rel_context in
   Renv.push_rels env (Array.of_list ids);
   let lam = lambda_of_constr env sigma c in
 (*  if Flags.vm_draw_opt () then begin
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 5afefeebd..fefc3222d 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -17,7 +17,8 @@ open Util
 open Names
 open Term
 open Declarations
-open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 (* The type of environments. *)
 
@@ -127,7 +128,7 @@ let env_of_rel n env =
 
 let push_named_context_val d (ctxt,vals) =
   let rval = ref VKnone in
-    Context.Named.add d ctxt, (get_id d,rval)::vals
+    Context.Named.add d ctxt, (NamedDecl.get_id d,rval)::vals
 
 let push_named d env =
 (*  if not (env.env_rel_context = []) then raise (ASSERT env.env_rel_context);
@@ -135,7 +136,7 @@ let push_named d env =
   let rval = ref VKnone in
   { env_globals = env.env_globals;
     env_named_context = Context.Named.add d env.env_named_context;
-    env_named_vals = (get_id d, rval) :: env.env_named_vals;
+    env_named_vals = (NamedDecl.get_id d, rval) :: env.env_named_vals;
     env_rel_context = env.env_rel_context;
     env_rel_val = env.env_rel_val;
     env_nb_rel = env.env_nb_rel;
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 09f7bd75c..f176ca579 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -62,6 +62,8 @@ open Names
 open Declarations
 open Context.Named.Declaration
 
+module NamedDecl = Context.Named.Declaration
+
 (** {6 Safe environments }
 
   Fields of [safe_environment] :
@@ -361,7 +363,7 @@ let check_required current_libs needed =
     cost too much. *)
 
 let safe_push_named d env =
-  let id = get_id d in
+  let id = NamedDecl.get_id d in
   let _ =
     try
       let _ = Environ.lookup_named id env in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 749b5dbaf..e59a17d12 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -22,6 +22,8 @@ open Entries
 open Typeops
 open Fast_typeops
 
+module NamedDecl = Context.Named.Declaration
+
 let constrain_type env j poly subst = function
   | `None -> 
     if not poly then (* Old-style polymorphism *)
@@ -254,13 +256,12 @@ let global_vars_set_constant_type env = function
       ctx ~init:Id.Set.empty
 
 let record_aux env s_ty s_bo suggested_expr =
-  let open Context.Named.Declaration in
   let in_ty = keep_hyps env s_ty in
   let v =
     String.concat " "
       (CList.map_filter (fun decl ->
-          let id = get_id decl in
-          if List.exists (Id.equal id % get_id) in_ty then None
+          let id = NamedDecl.get_id decl in
+          if List.exists (Id.equal id % NamedDecl.get_id) in_ty then None
           else Some (Id.to_string id))
         (keep_hyps env s_bo)) in
   Aux_file.record_in_aux "context_used" (v ^ ";" ^ suggested_expr)
@@ -269,9 +270,8 @@ let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
 let set_suggest_proof_using f = suggest_proof_using := f
 
 let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
-  let open Context.Named.Declaration in
   let check declared inferred =
-    let mk_set l = List.fold_right Id.Set.add (List.map get_id l) Id.Set.empty in
+    let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
     let inferred_set, declared_set = mk_set inferred, mk_set declared in
     if not (Id.Set.subset inferred_set declared_set) then
       let l = Id.Set.elements (Idset.diff inferred_set declared_set) in
@@ -283,12 +283,12 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
         fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in
   let sort evn l =
     List.filter (fun decl ->
-      let id = get_id decl in
-      List.exists (Names.Id.equal id % get_id) l)
+      let id = NamedDecl.get_id decl in
+      List.exists (Names.Id.equal id % NamedDecl.get_id) l)
     (named_context env) in
   (* We try to postpone the computation of used section variables *)
   let hyps, def =
-    let context_ids = List.map get_id (named_context env) in
+    let context_ids = List.map NamedDecl.get_id (named_context env) in
     match ctx with
     | None when not (List.is_empty context_ids) -> 
         (* No declared section vars, and non-empty section context:
@@ -482,8 +482,7 @@ let translate_local_def mb env id centry =
     | Undef _ -> ()
     | Def _ -> ()
     | OpaqueDef lc ->
-       let open Context.Named.Declaration in
-       let context_ids = List.map get_id (named_context env) in
+       let context_ids = List.map NamedDecl.get_id (named_context env) in
        let ids_typ = global_vars_set env typ in
        let ids_def = global_vars_set env
          (Opaqueproof.force_proof (opaque_tables env) lc) in
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 0059111c0..24018ab31 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -20,6 +20,9 @@ open Inductive
 open Type_errors
 open Context.Rel.Declaration
 
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
+
 let conv_leq l2r env x y = default_conv CUMUL ~l2r env x y
 
 let conv_leq_vecti env v1 v2 =
@@ -79,7 +82,7 @@ let judge_of_type u =
 
 let judge_of_relative env n =
   try
-    let typ = get_type (lookup_rel n env) in
+    let typ = RelDecl.get_type (lookup_rel n env) in
     { uj_val  = mkRel n;
       uj_type = lift n typ }
   with Not_found ->
@@ -102,7 +105,7 @@ let check_hyps_inclusion env c sign =
   Context.Named.fold_outside
     (fun d1 () ->
       let open Context.Named.Declaration in
-      let id = get_id d1 in
+      let id = NamedDecl.get_id d1 in
       try
         let d2 = lookup_named id env in
         conv env (get_type d2) (get_type d1);
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 2ca749d50..b27e27fda 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -8,7 +8,8 @@
 
 open Names
 open Esubst
-open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
 
 (*********************)
 (*     Occurring     *)
@@ -160,14 +161,15 @@ let substnl laml n c = substn_many (make_subst laml) n c
 let substl laml c = substn_many (make_subst laml) 0 c
 let subst1 lam c = substn_many [|make_substituend lam|] 0 c
 
-let substnl_decl laml k r = map_constr (fun c -> substnl laml k c) r
-let substl_decl laml r = map_constr (fun c -> substnl laml 0 c) r
-let subst1_decl lam r = map_constr (fun c -> subst1 lam c) r
+let substnl_decl laml k r = RelDecl.map_constr (fun c -> substnl laml k c) r
+let substl_decl laml r = RelDecl.map_constr (fun c -> substnl laml 0 c) r
+let subst1_decl lam r = RelDecl.map_constr (fun c -> subst1 lam c) r
 
 (* Build a substitution from an instance, inserting missing let-ins *)
 
 let subst_of_rel_context_instance sign l =
   let rec aux subst sign l =
+    let open RelDecl in
     match sign, l with
     | LocalAssum _ :: sign', a::args' -> aux (a::subst) sign' args'
     | LocalDef (_,c,_)::sign', args' ->