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, 8 insertions, 6 deletions

diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 9fff64ae5..c3cdb361b 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -17,6 +17,9 @@ open Util
 open Typeclasses_errors
 open Libobject
 open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
+module NamedDecl = Context.Named.Declaration
 (*i*)
 
 let typeclasses_unique_solutions = ref false
@@ -181,7 +184,7 @@ let subst_class (subst,cl) =
   let do_subst_con c = Mod_subst.subst_constant subst c
   and do_subst c = Mod_subst.subst_mps subst c
   and do_subst_gr gr = fst (subst_global subst gr) in
-  let do_subst_ctx = List.smartmap (map_constr do_subst) in
+  let do_subst_ctx = List.smartmap (RelDecl.map_constr do_subst) in
   let do_subst_context (grs,ctx) =
     List.smartmap (Option.smartmap (fun (gr,b) -> do_subst_gr gr, b)) grs,
     do_subst_ctx ctx in
@@ -198,16 +201,15 @@ let discharge_class (_,cl) =
   let repl = Lib.replacement_context () in
   let rel_of_variable_context ctx = List.fold_right
     ( fun (decl,_) (ctx', subst) ->
-        let open Context.Named.Declaration in
-        let decl' = decl |> map_constr (substn_vars 1 subst) |> to_rel in
-	(decl' :: ctx', Context.Named.Declaration.get_id decl :: subst)
+        let decl' = decl |> NamedDecl.map_constr (substn_vars 1 subst) |> NamedDecl.to_rel in
+	(decl' :: ctx', NamedDecl.get_id decl :: subst)
     ) ctx ([], []) in
   let discharge_rel_context subst n rel =
     let rel = Context.Rel.map (Cooking.expmod_constr repl) rel in
     let ctx, _ =
       List.fold_right
 	(fun decl (ctx, k) ->
-	   map_constr (substn_vars k subst) decl :: ctx, succ k
+	   RelDecl.map_constr (substn_vars k subst) decl :: ctx, succ k
 	)
 	rel ([], n)
     in ctx
@@ -220,7 +222,7 @@ let discharge_class (_,cl) =
   let discharge_context ctx' subst (grs, ctx) =
     let grs' =
       let newgrs = List.map (fun decl ->
-			     match decl |> get_type |> class_of_constr with
+			     match decl |> RelDecl.get_type |> class_of_constr with
 			     | None -> None
 			     | Some (_, ((tc,_), _)) -> Some (tc.cl_impl, true))
 			    ctx'