aboutsummaryrefslogtreecommitdiff
path: root/test-suite/bugs/closed/bug_8369.v
AgeCommit message (Collapse)Author
2019-01-06Reworking error message for unresolved evar subterm of another evar.Hugo Herbelin
This is a reworking of 7fd28dc9: instead of using words such as "domain of", "codomain of" to refer to a position in the instance of the original evar, we simply display the instance and the name of the unresolved evar in this instance. This is both simpler and more informative. (The positional words remain useful for printing the evar_map in debugging though.) In passing, this fixes #8369 (Not_found in printing message about an unresolved subevar). Incidentally add possible breaking while printing "in environment".