aboutsummaryrefslogtreecommitdiff
path: root/kernel/safe_typing.ml
diff options
context:
space:
mode:
authorMatej Kosik2016-08-13 18:11:22 +0200
committerMatej Kosik2016-08-24 21:12:29 +0200
commita5d336774c7b5342c8d873d43c9b92bae42b43e7 (patch)
tree1a1e4e6868c32222f94ee59257163d7d774ec9d0 /kernel/safe_typing.ml
parentd5d80dfc0f773fd6381ee4efefc74804d103fe4e (diff)
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.
Diffstat (limited to 'kernel/safe_typing.ml')
-rw-r--r--kernel/safe_typing.ml4
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 09f7bd75cd..f176ca5798 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -62,6 +62,8 @@ open Names
open Declarations
open Context.Named.Declaration
+module NamedDecl = Context.Named.Declaration
+
(** {6 Safe environments }
Fields of [safe_environment] :
@@ -361,7 +363,7 @@ let check_required current_libs needed =
cost too much. *)
let safe_push_named d env =
- let id = get_id d in
+ let id = NamedDecl.get_id d in
let _ =
try
let _ = Environ.lookup_named id env in