diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/constr_matching.ml | 2 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 4 |
2 files changed, 5 insertions, 1 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 2334be9664..edcfa99c86 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -361,6 +361,8 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PFix c1, Fix _ when eq_constr sigma (mkFix (to_fix c1)) cT -> subst | PCoFix c1, CoFix _ when eq_constr sigma (mkCoFix (to_fix c1)) cT -> subst + | PEvar (c1,args1), Evar (c2,args2) when Evar.equal c1 c2 -> + Array.fold_left2 (sorec ctx env) subst args1 args2 | _ -> raise PatternMatchingFailure in diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 33a68589c1..a22db1407b 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -159,7 +159,9 @@ let pattern_of_constr env sigma t = (match snd (Evd.evar_source evk sigma) with | Evar_kinds.MatchingVar (b,id) -> assert (not b); PMeta (Some id) - | Evar_kinds.GoalEvar -> + | Evar_kinds.GoalEvar | Evar_kinds.VarInstance _ -> + (* These are the two evar kinds used for existing goals *) + (* see Proofview.mark_in_evm *) PEvar (evk,Array.map (pattern_of_constr env) ctxt) | _ -> PMeta None) |