diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/mod_checking.ml | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 1dd16f1630..a3f151ef86 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -29,10 +29,16 @@ let check_constant_declaration env kn cb = in let ty = cb.const_type in let _ = infer_type env' ty in + let otab = Environ.opaque_tables env in + let body = match cb.const_body with + | Undef _ | Primitive _ -> None + | Def c -> Some (Mod_subst.force_constr c) + | OpaqueDef o -> Some (Opaqueproof.force_proof otab o) + in let () = - match Environ.body_of_constant_body env cb with + match body with | Some bd -> - let j = infer env' (fst bd) in + let j = infer env' bd in (try conv_leq env' j.uj_type ty with NotConvertible -> Type_errors.error_actual_type env j ty) | None -> () |