diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/retyping.ml | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index a49e2026a1..bb1a366376 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -45,6 +45,18 @@ let anomaly_on_error f x = try f x with RetypeError e -> anomaly ~label:"retyping" (print_retype_error e) +let get_type_from_constraints env sigma t = + if isEvar (fst (decompose_app t)) then + match + List.map_filter (fun (pbty,env,t1,t2) -> + 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 + | t::l -> t + | _ -> raise Not_found + else raise Not_found let rec subst_type env sigma typ = function | [] -> typ @@ -88,7 +100,12 @@ let retype ?(polyprop=true) sigma = | Construct cstr -> type_of_constructor env cstr | Case (_,p,c,lf) -> let Inductiveops.IndType(_,realargs) = - try Inductiveops.find_rectype env sigma (type_of env c) + let t = type_of env c in + try Inductiveops.find_rectype env sigma t + with Not_found -> + try + let t = get_type_from_constraints env sigma t in + Inductiveops.find_rectype env sigma t with Not_found -> retype_error BadRecursiveType in let t = whd_beta sigma (applist (p, realargs)) in |