From c3b9a7bf9fcd162628ce6a2a544652ca096cfe54 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 15 Oct 2016 16:27:37 +0200
Subject: Fix bug #5145: Anomaly: index to an anonymous variable.

When printing evar constraints, we ensure that every variable from the
rel context has a name.
---
 engine/evd.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine')

diff --git a/engine/evd.ml b/engine/evd.ml
index 6ba8a51120..291c089784 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1411,6 +1411,7 @@ let print_env_short env =
 
 let pr_evar_constraints pbs =
   let pr_evconstr (pbty, env, t1, t2) =
+    let env = Namegen.make_all_name_different env in
     print_env_short env ++ spc () ++ str "|-" ++ spc () ++
       print_constr_env env t1 ++ spc () ++
       str (match pbty with
-- 
cgit v1.2.3