diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2019-02-02 19:29:23 -0500 |
commit | 9ebf44d84754adc5b64fcf612c6816c02c80462d (patch) | |
tree | bf5e06a28488e0e06a2f2011ff0d110e2e02f8fc /checker/mod_checking.ml | |
parent | 9043add656177eeac1491a73d2f3ab92bec0013c (diff) |
Imported Upstream version 8.9.0upstream/8.9.0upstream
Diffstat (limited to 'checker/mod_checking.ml')
-rw-r--r-- | checker/mod_checking.ml | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 3ef2b340..6b2af71f 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -26,17 +26,12 @@ let check_constant_declaration env kn cb = push_context ~strict:false ctx env in let ty = cb.const_type in - let () = ignore(infer_type env' ty) in - let () = + let _ = infer_type env' ty in + let () = match body_of_constant cb with | Some bd -> - (match cb.const_proj with - | None -> let j = infer env' bd in - conv_leq env' j ty - | Some pb -> - let env' = add_constant kn cb env' in - let j = infer env' bd in - conv_leq env' j ty) + let j = infer env' bd in + conv_leq env' j ty | None -> () in let env = |