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 e9fc74600e..69ca45444c 100644
--- a/engine/evd.ml
+++ b/engine/evd.ml
@@ -1410,6 +1410,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