diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 20:27:37 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-05 20:27:37 +0200 |
| commit | 66acf05f6fd0a35b7d9a0d425983c36dbe2cc992 (patch) | |
| tree | d67a1ead218ca15becb33b605426cb5429323b60 /checker/typeops.ml | |
| parent | 0d7cd6eebd5b681f7dcb243e3cda4466e735e025 (diff) | |
Fix checker treatment of inductives using subst_instances instead of subst_univs_levels.
Diffstat (limited to 'checker/typeops.ml')
| -rw-r--r-- | checker/typeops.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/checker/typeops.ml b/checker/typeops.ml index 77fc4af73..f69f10295 100644 --- a/checker/typeops.ml +++ b/checker/typeops.ml @@ -224,8 +224,7 @@ let judge_of_projection env p c ct = with Not_found -> error_case_not_inductive env (c, ct) in assert(eq_mind pb.proj_ind (fst ind)); - let usubst = make_inductive_subst (fst (lookup_mind_specif env ind)) u in - let ty = subst_univs_level_constr usubst pb.proj_type in + let ty = subst_instance_constr u pb.proj_type in substl (c :: List.rev args) ty (* Fixpoints. *) @@ -392,8 +391,9 @@ let check_ctxt env rels = (* Polymorphic arities utils *) let check_kind env ar u = - if snd (dest_prod env ar) = Sort(Type u) then () - else failwith "not the correct sort" + match (snd (dest_prod env ar)) with + | Sort (Type u') when Univ.Universe.equal u' (Univ.Universe.make u) -> () + | _ -> failwith "not the correct sort" let check_polymorphic_arity env params par = let pl = par.template_param_levels in |