diff options
Diffstat (limited to 'pretyping/cases.ml')
-rw-r--r-- | pretyping/cases.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 04f50d50e..882c052f6 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1381,7 +1381,7 @@ and match_current pb (initial,tomatch) = let case = make_case_or_project pb.env indf ci pred current brvals in - Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; + Typing.check_allowed_sort pb.env !(pb.evdref) mind (EConstr.of_constr current) (EConstr.of_constr pred); { uj_val = applist (case, inst); uj_type = prod_applist typ inst } @@ -1684,7 +1684,7 @@ let build_tycon loc env tycon_env s subst tycon extenv evdref t = (lift (n'-n) impossible_case_type, mkSort u) | Some t -> let t = abstract_tycon loc tycon_env evdref subst tycon extenv t in - let evd,tt = Typing.type_of extenv !evdref t in + let evd,tt = Typing.type_of extenv !evdref (EConstr.of_constr t) in evdref := evd; (t,tt) in let b = e_cumul env evdref (EConstr.of_constr tt) (EConstr.mkSort s) (* side effect *) in @@ -1920,7 +1920,7 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = assert (len == 0); let p = predicate 0 c in let env' = List.fold_right push_rel_context arsign env in - try let sigma' = fst (Typing.type_of env' sigma p) in + try let sigma' = fst (Typing.type_of env' sigma (EConstr.of_constr p)) in Some (sigma', p) with e when precatchable_exception e -> None @@ -2041,7 +2041,7 @@ let constr_of_pat env evdref arsign pat avoid = let IndType (indf, _) = try find_rectype env ( !evdref) (EConstr.of_constr (lift (-(List.length realargs)) ty)) with Not_found -> error_case_not_inductive env !evdref - {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref ty} + {uj_val = ty; uj_type = Typing.unsafe_type_of env !evdref (EConstr.of_constr ty)} in let (ind,u), params = dest_ind_family indf in if not (eq_ind ind cind) then error_bad_constructor ~loc:l env cstr ind; @@ -2242,7 +2242,7 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity = let j = typing_fun (mk_tycon (EConstr.of_constr tycon)) rhs_env eqn.rhs.it in let bbody = it_mkLambda_or_LetIn j.uj_val rhs_rels' and btype = it_mkProd_or_LetIn j.uj_type rhs_rels' in - let _btype = evd_comb1 (Typing.type_of env) evdref bbody in + let _btype = evd_comb1 (Typing.type_of env) evdref (EConstr.of_constr bbody) in let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in let branch = |