diff options
Diffstat (limited to 'pretyping/vnorm.ml')
| -rw-r--r-- | pretyping/vnorm.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index 16eeaa293..2cf730f11 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -98,7 +98,8 @@ let construct_of_constr_block = construct_of_constr false let constr_type_of_idkey env idkey = match idkey with | ConstKey cst -> - mkConst cst, (Environ.lookup_constant cst env).const_type + let const_type = (Environ.lookup_constant cst env).const_type in + mkConst cst, Typeops.type_of_constant_type env const_type | VarKey id -> let (_,_,ty) = lookup_named id env in mkVar id, ty |