diff options
Diffstat (limited to 'pretyping/retyping.ml')
| -rw-r--r-- | pretyping/retyping.ml | 23 |
1 files changed, 9 insertions, 14 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 3582b644..7e43c5e4 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -57,8 +57,8 @@ let get_type_from_constraints env sigma t = if isEvar sigma (fst (decompose_app_vect sigma t)) then match List.map_filter (fun (pbty,env,t1,t2) -> - if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t1) then Some t2 - else if is_fconv Reduction.CONV env sigma t (EConstr.of_constr t2) then Some t1 + if is_fconv Reduction.CONV env sigma t t1 then Some t2 + else if is_fconv Reduction.CONV env sigma t t2 then Some t1 else None) (snd (Evd.extract_all_conv_pbs sigma)) with @@ -99,7 +99,7 @@ let retype ?(polyprop=true) sigma = let rec type_of env cstr = match EConstr.kind sigma cstr with | Meta n -> - (try strip_outer_cast sigma (EConstr.of_constr (Evd.meta_ftype sigma n).Evd.rebus) + (try strip_outer_cast sigma (Evd.meta_ftype sigma n).Evd.rebus with Not_found -> retype_error (BadMeta n)) | Rel n -> let ty = RelDecl.get_type (lookup_rel n env) in @@ -115,7 +115,7 @@ let retype ?(polyprop=true) sigma = try Inductiveops.find_rectype env sigma t with Not_found -> try - let t = EConstr.of_constr (get_type_from_constraints env sigma t) in + let t = get_type_from_constraints env sigma t in Inductiveops.find_rectype env sigma t with Not_found -> retype_error BadRecursiveType in @@ -149,18 +149,13 @@ let retype ?(polyprop=true) sigma = | Cast (c,_, s) when isSort sigma s -> destSort sigma s | Sort s -> begin match ESorts.kind sigma s with - | Prop _ -> Sorts.type1 + | Prop | Set -> Sorts.type1 | Type u -> Type (Univ.super u) end | Prod (name,t,c2) -> - (match (sort_of env t, sort_of (push_rel (LocalAssum (name,t)) env) c2) with - | _, (Prop Null as s) -> s - | Prop _, (Prop Pos as s) -> s - | Type _, (Prop Pos as s) when is_impredicative_set env -> s - | Type u1, Prop Pos -> Type (Univ.sup u1 Univ.type0_univ) - | Prop Pos, (Type u2) -> Type (Univ.sup Univ.type0_univ u2) - | Prop Null, (Type _ as s) -> s - | Type u1, Type u2 -> Type (Univ.sup u1 u2)) + let dom = sort_of env t in + let rang = sort_of (push_rel (LocalAssum (name,t)) env) c2 in + Typeops.sort_of_product env dom rang | App(f,args) when is_template_polymorphic env sigma f -> let t = type_of_global_reference_knowing_parameters env f args in sort_of_atomic_type env sigma t args @@ -170,7 +165,7 @@ let retype ?(polyprop=true) sigma = and type_of_global_reference_knowing_parameters env c args = let argtyps = - Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in + Array.map (fun c -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma (type_of env c))) args in match EConstr.kind sigma c with | Ind (ind, u) -> let u = EInstance.kind sigma u in |