aboutsummaryrefslogtreecommitdiff
path: root/engine
diff options
context:
space:
mode:
Diffstat (limited to 'engine')
-rw-r--r--engine/evd.ml1
1 files changed, 1 insertions, 0 deletions
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