diff options
| author | Hugo Herbelin | 2014-10-17 15:17:07 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-10-17 15:17:11 +0200 |
| commit | b1b8243b7fc0bd8e2b9db3ddb28941646b3bd1ff (patch) | |
| tree | 9eb1291740667410dcbc9a6e82cdb8d69c42eac5 | |
| parent | cfff8f8a32708ea0c8e72178424db0b40665fe37 (diff) | |
When facing problem ?id = ?id' in resolution of return predicate,
early call the standard resolution function which e.g. does
restriction and maybe solve the problem if pattern-like, instead of
postponing the problem.
| -rw-r--r-- | pretyping/cases.ml | 9 |
1 files changed, 6 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 411f2c550f..78837b9d8c 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1604,9 +1604,12 @@ let abstract_tycon loc env evdref subst _tycon extenv t = (fun i _ -> try list_assoc_in_triple i subst0 with Not_found -> mkRel i) 1 (rel_context env) in - let ev = e_new_evar env evdref ~src:(loc, Evar_kinds.CasesType) ty in - evdref := add_conv_pb (Reduction.CONV,env,substl inst ev,t) !evdref; - ev + let ev' = e_new_evar env evdref ~src:(loc, Evar_kinds.CasesType) ty in + begin match solve_simple_eqn (evar_conv_x full_transparent_state) env !evdref (None,ev,substl inst ev') with + | Success evd -> evdref := evd + | UnifFailure _ -> assert false + end; + ev' | _ -> let good = List.filter (fun (_,u,_) -> is_conv_leq env sigma t u) subst in match good with |