From 18626b09a8a8ea1d56a7f91f347e1ebb3960e2c6 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 23 Dec 2019 20:22:29 +0100
Subject: 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.
---
 vernac/himsg.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'vernac')

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" ++
-- 
cgit v1.2.3