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, 2 deletions

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);