aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/5097.v
AgeCommit message (Collapse)Author
2018-10-04rename test files (do not start by a digit)Vincent Laporte
2016-10-20A fix for #5097 (status of evars refined by "clear" in ltac: closed wrt evars).Hugo Herbelin
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".