aboutsummaryrefslogtreecommitdiff
path: root/doc/plugin_tutorial/tuto0
diff options
context:
space:
mode:
authorHugo Herbelin2018-08-31 18:51:04 +0200
committerHugo Herbelin2019-01-06 19:56:51 +0100
commit0703cd1bbe5aab7e584d2293fe76c5f6ac4fe08c (patch)
tree70a351adacba425619d431bb58bcbfb4d49be1ee /doc/plugin_tutorial/tuto0
parent3d7eb01d428c9d98b10004f3f4f40b2209232971 (diff)
Reworking error message for unresolved evar subterm of another evar.
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".
Diffstat (limited to 'doc/plugin_tutorial/tuto0')
0 files changed, 0 insertions, 0 deletions