From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001 From: Benjamin Barenblat Date: Sat, 2 Feb 2019 19:29:23 -0500 Subject: Imported Upstream version 8.9.0 --- checker/mod_checking.ml | 13 ++++--------- 1 file changed, 4 insertions(+), 9 deletions(-) (limited to 'checker/mod_checking.ml') 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 = -- cgit v1.2.3