diff options
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index e52112fda..27e457e3b 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -184,7 +184,7 @@ let pattern_of_constr env sigma t = | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> (* These are the two evar kinds used for existing goals *) (* see Proofview.mark_in_evm *) - if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value sigma ev) + if Evd.is_defined sigma evk then pattern_of_constr env (Evd.existential_value0 sigma ev) else PEvar (evk,Array.map (pattern_of_constr env) ctxt) | Evar_kinds.MatchingVar (Evar_kinds.SecondOrderPatVar ido) -> assert false | _ -> |