diff options
| author | Maxime Dénès | 2017-05-02 16:22:10 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-02 16:22:10 +0200 |
| commit | 510701319b1b0420698e411e24022a0fbec7c36c (patch) | |
| tree | ef075e85ce6a2dd3002a356c8a5cd738de72f0dd /pretyping | |
| parent | 1f2303052c5422699db2ef7673b35fae42108114 (diff) | |
| parent | c3aec655a8a33fff676c79e12888d193cc2e237b (diff) | |
Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/constr_matching.ml | 3 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 4 |
2 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 3c47cfdc4b..afdf601c21 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -347,6 +347,9 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | PFix c1, Fix _ when eq_constr (mkFix c1) cT -> subst | PCoFix c1, CoFix _ when eq_constr (mkCoFix c1) cT -> subst + | PEvar (c1,args1), Evar (c2,args2) when 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 2090aad8a0..75d3ed30ba 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -160,7 +160,9 @@ let pattern_of_constr env sigma t = let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in let () = ignore (pattern_of_constr env ty) in 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) | _ -> let ty = Evarutil.nf_evar sigma (existential_type sigma ev) in |