diff options
Diffstat (limited to 'kernel/subtyping.ml')
| -rw-r--r-- | kernel/subtyping.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 2a81ebee0b..6e20ceeb4c 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -160,9 +160,10 @@ let check_constant cst env msid1 l info1 cb2 spec2 = let cst = check_conv cst conv_leq env cb1.const_type cb2.const_type in match cb2.const_body with | None -> cst - | Some c2 -> + | Some lc2 -> + let c2 = Lazy.force_val lc2 in let c1 = match cb1.const_body with - | Some c1 -> c1 + | Some c1 -> Lazy.force_val c1 | None -> mkConst (make_kn (MPself msid1) empty_dirpath l) in check_conv cst conv env c1 c2 |