diff options
author | 2017-04-28 16:30:45 +0200 | |
---|---|---|
committer | 2017-04-28 16:37:12 +0200 | |
commit | 68fb8e13c44c5ee95dbc9256b1d74c7c83303d2d (patch) | |
tree | 9b464872424a3b0fd01181f1b85b05e0b7112d75 /test-suite | |
parent | 9a91a385b2562a0656edf8766f229dc8120b2675 (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...
Diffstat (limited to 'test-suite')
-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. |