aboutsummaryrefslogtreecommitdiff
path: root/kernel/fast_typeops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/fast_typeops.ml')
-rw-r--r--kernel/fast_typeops.ml3
1 files changed, 1 insertions, 2 deletions
diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml
index df95c93dc5..7f4ba8ecbe 100644
--- a/kernel/fast_typeops.ml
+++ b/kernel/fast_typeops.ml
@@ -74,8 +74,7 @@ let judge_of_type u =
let judge_of_relative env n =
try
let open Context.Rel.Declaration in
- let typ = get_type (lookup_rel n env) in
- lift n typ
+ env |> lookup_rel n |> get_type |> lift n
with Not_found ->
error_unbound_rel env n