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.

1 files changed, 5 insertions, 4 deletions

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