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 | |
| parent | 1f2303052c5422699db2ef7673b35fae42108114 (diff) | |
| parent | c3aec655a8a33fff676c79e12888d193cc2e237b (diff) | |
Merge PR#597: Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
| -rw-r--r-- | pretyping/constr_matching.ml | 3 | ||||
| -rw-r--r-- | pretyping/patternops.ml | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/5487.v | 9 | ||||
| -rw-r--r-- | test-suite/success/ltac.v | 13 |
4 files changed, 28 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 diff --git a/test-suite/bugs/closed/5487.v b/test-suite/bugs/closed/5487.v new file mode 100644 index 0000000000..9b995f4503 --- /dev/null +++ b/test-suite/bugs/closed/5487.v @@ -0,0 +1,9 @@ +(* Was a collision between an ltac pattern variable and an evar *) + +Goal forall n, exists m, n = m :> nat. +Proof. + eexists. + Fail match goal with + | [ |- ?x = ?y ] + => match x with y => idtac end + end. diff --git a/test-suite/success/ltac.v b/test-suite/success/ltac.v index ce90990594..d7ec092d76 100644 --- a/test-suite/success/ltac.v +++ b/test-suite/success/ltac.v @@ -317,3 +317,16 @@ let T := constr:(fun a b : nat => a) in end. exact (eq_refl n). Qed. + +(* A variant of #2602 which was wrongly succeeding because "a", bound to + "?m", was then internally turned into a "_" in the second matching *) + +Goal exists m, S m > 0. +eexists. +Fail match goal with + | |- context [ S ?a ] => + match goal with + | |- S a > a => idtac + end +end. +Abort. |