CLEANUP: removing superfluous (module) qualifiers

2 files changed, 5 insertions, 3 deletions

diff --git a/library/impargs.ml b/library/impargs.ml
index 3ddef3a9ae..cda1a662b4 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -515,11 +515,12 @@ 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 (Context.Named.Declaration.get_id decl, Manual, (true, true))
+  | Implicit -> Some (get_id decl, Manual, (true, true))
   | _ -> None
   in
-  let is_set = Context.Named.Declaration.is_local_assum % fst in
+  let is_set = is_local_assum % fst in
   List.rev_map map (List.filter is_set ctx)
 
 let adjust_side_condition p = function
diff --git a/pretyping/arguments_renaming.ml b/pretyping/arguments_renaming.ml
index bf9063fdbc..fe10737623 100644
--- a/pretyping/arguments_renaming.ml
+++ b/pretyping/arguments_renaming.ml
@@ -48,7 +48,8 @@ let discharge_rename_args = function
      (try 
        let vars,_,_ = section_segment_of_reference c in
        let c' = pop_global_reference c in
-       let var_names = List.map (Name.mk_name % Context.Named.Declaration.get_id % fst) vars in
+       let open Context.Named.Declaration in
+       let var_names = List.map (Name.mk_name % get_id % fst) vars in
        let names' = List.map (fun l -> var_names @ l) names in
        Some (ReqGlobal (c', names), (c', names'))
      with Not_found -> Some req)