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 /vernac/himsg.ml | |
| 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 'vernac/himsg.ml')
| -rw-r--r-- | vernac/himsg.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/himsg.ml b/vernac/himsg.ml index 19ec0a3642..085689be0a 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -297,6 +297,7 @@ let explain_unification_error env sigma p1 p2 = function strbrk " with term " ++ pr_leconstr_env env sigma rhs ++ strbrk " that would depend on itself"] | NotClean ((evk,args),env,c) -> + let env = make_all_name_different env sigma in [str "cannot instantiate " ++ quote (pr_existential_key sigma evk) ++ strbrk " because " ++ pr_leconstr_env env sigma c ++ strbrk " is not in its scope" ++ |