diff options
| author | Hugo Herbelin | 2017-04-28 16:30:45 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-28 16:37:12 +0200 |
| commit | 68fb8e13c44c5ee95dbc9256b1d74c7c83303d2d (patch) | |
| tree | 9b464872424a3b0fd01181f1b85b05e0b7112d75 /dev | |
| 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 'dev')
0 files changed, 0 insertions, 0 deletions