diff options
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 = |