diff options
| -rw-r--r-- | pretyping/cases.ml | 10 | ||||
| -rw-r--r-- | pretyping/coercion.ml | 9 |
2 files changed, 14 insertions, 5 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 6559084578..163d37f964 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1655,13 +1655,15 @@ let prepare_predicate loc typing_fun sigma env tomatchs sign tycon pred = (* Some type annotation *) | Some rtntyp, _ -> (* We extract the signature of the arity *) - let env = List.fold_right push_rels arsign env in + let envar = List.fold_right push_rels arsign env in let sigma, newt = new_sort_variable sigma in let evdref = ref sigma in - let predcclj = typing_fun (mk_tycon (mkSort newt)) env evdref rtntyp in + let predcclj = typing_fun (mk_tycon (mkSort newt)) envar evdref rtntyp in let sigma = Option.cata (fun tycon -> - let tycon = lift_tycon_type (List.length arsign) tycon in - Coercion.inh_conv_coerces_to loc env !evdref predcclj.uj_val tycon) + let na = (Name (id_of_string "x"),KnownNotDep) in + let tms = List.map (fun tm -> Pushed(tm,[],na)) tomatchs in + let predinst = extract_predicate [] predcclj.uj_val tms in + Coercion.inh_conv_coerces_to loc env !evdref predinst tycon) !evdref tycon in let predccl = (j_nf_evar sigma predcclj).uj_val in [sigma, KnownDep, predccl] diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 389761aeb9..553c912747 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -242,7 +242,14 @@ module Default = struct let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true - let inh_conv_coerces_to loc env (evd : evar_map) t (abs, t') = evd + let inh_conv_coerces_to loc env (evd : evar_map) t (abs, t') = + if abs = None then + try + fst (inh_conv_coerce_to_fail loc env evd true None t t') + with NoCoercion -> + evd (* Maybe not enough information to unify *) + else + evd (* Still problematic, as it changes unification let nabsinit, nabs = match abs with |