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.

3 files changed, 16 insertions, 16 deletions

diff --git a/library/decls.ml b/library/decls.ml
index 6e21880f1..2952c258a 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -14,6 +14,8 @@ open Names
 open Decl_kinds
 open Libnames
 
+module NamedDecl = Context.Named.Declaration
+
 (** Datas associated to section variables and local definitions *)
 
 type variable_data =
@@ -46,20 +48,18 @@ let constant_kind kn = Cmap.find kn !csttab
 
 (** Miscellaneous functions. *)
 
-open Context.Named.Declaration
-
 let initialize_named_context_for_proof () =
   let sign = Global.named_context () in
   List.fold_right
     (fun d signv ->
-      let id = get_id d in
-      let d = if variable_opacity id then LocalAssum (id, get_type d) else d in
+      let id = NamedDecl.get_id d in
+      let d = if variable_opacity id then NamedDecl.LocalAssum (id, NamedDecl.get_type d) else d in
       Environ.push_named_context_val d signv) sign Environ.empty_named_context_val
 
 let last_section_hyps dir =
   Context.Named.fold_outside
     (fun d sec_ids ->
-      let id = get_id d in
+      let id = NamedDecl.get_id d in
       try if DirPath.equal dir (variable_path id) then id::sec_ids else sec_ids
       with Not_found -> sec_ids)
     (Environ.named_context (Global.env()))
diff --git a/library/impargs.ml b/library/impargs.ml
index cda1a662b..e922ab773 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -22,6 +22,9 @@ open Constrexpr
 open Termops
 open Namegen
 open Decl_kinds
+open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 (*s Flags governing the computation of implicit arguments *)
 
@@ -164,7 +167,6 @@ let update pos rig (na,st) =
 
 (* modified is_rigid_reference with a truncated env *)
 let is_flexible_reference env bound depth f =
-  let open Context.Named.Declaration in
   match kind_of_term f with
     | Rel n when n >= bound+depth -> (* inductive type *) false
     | Rel n when n >= depth -> (* previous argument *) true
@@ -449,8 +451,7 @@ let compute_all_mib_implicits flags manual kn =
 
 let compute_var_implicits flags manual id =
   let env = Global.env () in
-  let open Context.Named.Declaration in
-  compute_semi_auto_implicits env flags manual (get_type (lookup_named id env))
+  compute_semi_auto_implicits env flags manual (NamedDecl.get_type (lookup_named id env))
 
 (* Implicits of a global reference. *)
 
@@ -515,13 +516,11 @@ let subst_implicits (subst,(req,l)) =
   (ImplLocal,List.smartmap (subst_implicits_decl subst) l)
 
 let impls_of_context ctx =
-  let open Context.Named.Declaration in
   let map (decl, impl) = match impl with
-  | Implicit -> Some (get_id decl, Manual, (true, true))
+  | Implicit -> Some (NamedDecl.get_id decl, Manual, (true, true))
   | _ -> None
   in
-  let is_set = is_local_assum % fst in
-  List.rev_map map (List.filter is_set ctx)
+  List.rev_map map (List.filter (is_local_assum % fst) ctx)
 
 let adjust_side_condition p = function
   | LessArgsThan n -> LessArgsThan (n+p)
diff --git a/library/lib.ml b/library/lib.ml
index 7fc3e0d9c..412772e8a 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -13,6 +13,9 @@ open Libnames
 open Globnames
 open Nameops
 open Libobject
+open Context.Named.Declaration
+
+module NamedDecl = Context.Named.Declaration
 
 type is_type = bool (* Module Type or just Module *)
 type export = bool option (* None for a Module Type *)
@@ -428,9 +431,8 @@ let add_section_context ctx =
        sectab := (Context ctx :: vars,repl,abs)::sl
 
 let extract_hyps (secs,ohyps) =
-  let open Context.Named.Declaration in
   let rec aux = function
-    | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (get_id decl) ->
+    | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
       let l, r = aux (idl,hyps) in 
       (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r
     | (Variable (_,_,poly,ctx)::idl,hyps) ->
@@ -443,8 +445,7 @@ let extract_hyps (secs,ohyps) =
   in aux (secs,ohyps)
 
 let instance_from_variable_context =
-  let open Context.Named.Declaration in
-  Array.of_list % List.map get_id % List.filter is_local_assum % List.map fst
+  Array.of_list % List.map NamedDecl.get_id % List.filter is_local_assum % List.map fst
 
 let named_of_variable_context =
   List.map fst