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. --- pretyping/nativenorm.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'pretyping/nativenorm.ml') diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml index 0dd64697c..ffb9f8940 100644 --- a/pretyping/nativenorm.ml +++ b/pretyping/nativenorm.ml @@ -20,6 +20,8 @@ open Nativecode open Nativevalues open Context.Rel.Declaration +module RelDecl = Context.Rel.Declaration + (** This module implements normalization by evaluation to OCaml code *) exception Find_at of int @@ -122,7 +124,7 @@ let build_case_type dep p realargs c = (* TODO move this function *) let type_of_rel env n = - lookup_rel n env |> get_type |> lift n + lookup_rel n env |> RelDecl.get_type |> lift n let type_of_prop = mkSort type1_sort -- cgit v1.2.3