diff options
| author |  Amin Timany <amintimany@gmail.com> | 2017-06-01 16:18:19 +0200 |
|---|---|---|
| committer |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-06-16 04:51:19 +0200 |
| commit | ff918e4bb0ae23566e038f4b55d84dd2c343f95e (patch) | |
| tree | ebab76cc4dedaf307f96088a3756d8292a341433 /checker/mod_checking.ml | |
| parent | 3380f47d2bb38d549fcdac8fb073f9aa1f259a23 (diff) | |
Clean up universes of constants and inductives
Diffstat (limited to 'checker/mod_checking.ml')
| -rw-r--r-- | checker/mod_checking.ml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index 7f93e1560..15e9ae295 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -1,4 +1,3 @@ - open Pp open Util open Names @@ -26,21 +25,23 @@ let refresh_arity ar = | _ -> ar, Univ.ContextSet.empty let check_constant_declaration env kn cb = - Flags.if_verbose Feedback.msg_notice (str " checking cst: " ++ prcon kn); - let env' = - if cb.const_polymorphic then - let inst = Univ.make_abstract_instance cb.const_universes in - let ctx = Univ.UContext.make (inst, Univ.UContext.constraints cb.const_universes) in - push_context ~strict:false ctx env - else push_context ~strict:true cb.const_universes env + Feedback.msg_notice (str " checking cst:" ++ prcon kn); + let env', u = + match cb.const_universes with + | Monomorphic_const ctx -> push_context ~strict:true ctx env, Univ.Instance.empty + | Polymorphic_const auctx -> + let ctx = Univ.instantiate_univ_context auctx in + push_context ~strict:false ctx env, Univ.UContext.instance ctx in let envty, ty = match cb.const_type with RegularArity ty -> + let ty = subst_instance_constr u ty in 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) -> + assert(Univ.Instance.is_empty u); let _ = check_ctxt env' ctxt in check_polymorphic_arity env' ctxt par; env', it_mkProd_or_LetIn (Sort(Type par.template_level)) ctxt @@ -48,6 +49,7 @@ let check_constant_declaration env kn cb = let () = match body_of_constant cb with | Some bd -> + let bd = subst_instance_constr u bd in (match cb.const_proj with | None -> let j = infer envty bd in conv_leq envty j ty @@ -57,7 +59,7 @@ let check_constant_declaration env kn cb = conv_leq envty j ty) | None -> () in - if cb.const_polymorphic then add_constant kn cb env + if constant_is_polymorphic cb then add_constant kn cb env else add_constant kn cb env' (** {6 Checking modules } *) |