diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-09-24 16:37:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2016-10-20 20:22:07 +0200 |
| commit | a07f67f6f1deba8b14672c618c003ec345d7970a (patch) | |
| tree | c9f33707c6c7dc3fae71d1e0a7e35e5686751a5d /test-suite/bugs/4623.v | |
| parent | 317ae3b327d201530730ed2cce5f44e8763814d4 (diff) | |
A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars).
If an existing evar was cleared in pretyping (typically while
processing "ltac:"), it created an evar considered as new. Updating
them instead along the "cleared" flag.
If correct, I suspect similar treatment should be done for refining
along "change", "rename" and "move".
Diffstat (limited to 'test-suite/bugs/4623.v')
0 files changed, 0 insertions, 0 deletions