diff options
| author | Hugo Herbelin | 2019-12-23 20:22:29 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-23 22:52:29 +0100 |
| commit | 18626b09a8a8ea1d56a7f91f347e1ebb3960e2c6 (patch) | |
| tree | e2480d799590b4411406bdec884c8adcc8625f97 /dev | |
| parent | 9c75b6a6582620e2fb9a39c1ea1aa46a321af6a7 (diff) | |
Fixes a small bug exposing an _ANONYMOUS_REL in a unification error message.
Might be improvable further. In the first example, we have two
environments involved and one is implicit. It does not seem excluded
that a variable name of the second environment shows up which is not
listed in the first environment.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions