diff options
| author | coq | 2002-10-05 11:03:20 +0000 |
|---|---|---|
| committer | coq | 2002-10-05 11:03:20 +0000 |
| commit | 1e485645ef6481a856e8a67477f186519fb8ec9d (patch) | |
| tree | fe06414569b65ae325c474f55e831fe228a0c23c /kernel/subtyping.ml | |
| parent | dfb48b895bb114e6eb49840d960268e18f8aaf0c (diff) | |
Lazy experimentale temporaire...
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |