From d7db69dea59cddd3ac81ed469170fad889af4e16 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Sat, 6 Sep 2014 09:30:16 +0200 Subject: Fix checking of constants in checker. Prelude can now be checked. --- checker/mod_checking.ml | 33 +++++++++++++++++++-------------- 1 file changed, 19 insertions(+), 14 deletions(-) (limited to 'checker/mod_checking.ml') diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 12a97bf68..93b136c48 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -25,22 +25,27 @@ let refresh_arity ar = let check_constant_declaration env kn cb = Flags.if_verbose ppnl (str " checking cst: " ++ prcon kn); - let env = add_constraints (Univ.UContext.constraints cb.const_universes) env in - (match cb.const_type with + let env' = add_constraints (Univ.UContext.constraints cb.const_universes) env in + let envty, ty = + match cb.const_type with RegularArity ty -> - let ty, cu = refresh_arity ty in - let envty = add_constraints cu env in - let _ = infer_type envty ty in - (match body_of_constant cb with - | Some bd -> - let j = infer envty bd in - conv_leq envty j ty - | None -> ()) + let ty', cu = refresh_arity ty in + let envty = add_constraints 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); - add_constant kn cb env - + let _ = check_ctxt env' ctxt in + check_polymorphic_arity env' ctxt par; + env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt + in + let body = + match body_of_constant cb with + | Some bd -> + let j = infer envty bd in + conv_leq envty j ty + | None -> () + in + if cb.const_polymorphic then add_constant kn cb env + else add_constant kn cb env' (** {6 Checking modules } *) -- cgit v1.2.3