From 66acf05f6fd0a35b7d9a0d425983c36dbe2cc992 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 5 Sep 2014 20:27:37 +0200 Subject: Fix checker treatment of inductives using subst_instances instead of subst_univs_levels. --- checker/typeops.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'checker/typeops.ml') 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 -- cgit v1.2.3