diff options
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 4948f6008..b6816dd48 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -35,15 +35,11 @@ let check_constant_declaration env kn cb = push_context ~strict:false ctx env in let envty, ty = - match cb.const_type with - RegularArity ty -> - let ty', cu = refresh_arity ty in - let envty = push_context_set cu env' in - let _ = infer_type envty ty' in envty, ty - | TemplateArity(ctxt,par) -> - let _ = check_ctxt env' ctxt in - check_polymorphic_arity env' ctxt par; - env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt + let ty = cb.const_type in + let ty', cu = refresh_arity ty in + let envty = push_context_set cu env' in + let _ = infer_type envty ty' in + envty, ty in let () = match body_of_constant cb with |