diff options
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 668c2770d2..7baa755ab5 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -406,9 +406,14 @@ let coerce_to_indtype typing_fun evdref env matx tomatchl = (* Utils *) let mkExistential env ?(src=(Loc.tag Evar_kinds.InternalHole)) evdref = - let (e, u) = evd_comb1 (new_type_evar env ~src:src) evdref univ_flexible_alg in + let (e, u) = evd_comb1 (new_type_evar env ~src:src) evdref univ_flexible_alg in e +let evd_comb2 f evdref x y = + let (evd',y) = f !evdref x y in + evdref := evd'; + y + let adjust_tomatch_to_pattern pb ((current,typ),deps,dep) = (* Ideally, we could find a common inductive type to which both the term to match and the patterns coerce *) |