diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-01 16:58:38 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-05-01 17:06:39 +0200 |
| commit | c3aec655a8a33fff676c79e12888d193cc2e237b (patch) | |
| tree | 960f22ca0c2f3f148ecf8cf99aa7333dad9fdcbc /test-suite/bugs/closed | |
| parent | 12f1c409daf2cdbd7d0323f0d61723819532b362 (diff) | |
Fixing #5487 (v8.5 regression on ltac-matching expressions with evars).
The fix follows an invariant enforced in proofview.ml on the kind of
evars that are goals or that occur in goals.
One day, evar kinds will need a little cleaning...
PS: This is a second attempt, completing db28e82 which was missing the
case PEvar in constr_matching.ml. Indeed the attached fix to #5487
alone made #2602 failing, revealing that the real cause for #2602 was
actually not fixed and that if the test for #2602 was working it was
because of #5487 hiding the real problem in #2602.
Diffstat (limited to 'test-suite/bugs/closed')
| -rw-r--r-- | test-suite/bugs/closed/5487.v | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/5487.v b/test-suite/bugs/closed/5487.v new file mode 100644 index 000000000..9b995f450 --- /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. |