diff options
| -rw-r--r-- | pretyping/patternops.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 009b7323e4..9fb6ec9d11 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -171,7 +171,10 @@ let pattern_of_constr env sigma t = assert (not b); PMeta (Some id) | Evar_kinds.GoalEvar -> PEvar (evk,Array.map (pattern_of_constr env) ctxt) - | _ -> PMeta None) + | _ -> + let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in + remove := Evar.Set.union (evars_of_term ty) !remove; + PMeta None) | Case (ci,p,a,br) -> let cip = { cip_style = ci.ci_pp_info.style; |