From a5d336774c7b5342c8d873d43c9b92bae42b43e7 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Sat, 13 Aug 2016 18:11:22 +0200 Subject: 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. --- kernel/typeops.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'kernel/typeops.ml') 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); -- cgit v1.2.3