aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/evd.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 822a3cb7c0..028361185e 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1777,11 +1777,11 @@ let print_env_short env =
let pr_evar_constraints pbs =
let pr_evconstr (pbty, env, t1, t2) =
print_env_short env ++ spc () ++ str "|-" ++ spc () ++
- print_constr t1 ++ spc () ++
+ print_constr_env env t1 ++ spc () ++
str (match pbty with
| Reduction.CONV -> "=="
| Reduction.CUMUL -> "<=") ++
- spc () ++ print_constr t2
+ spc () ++ print_constr_env env t2
in
prlist_with_sep fnl pr_evconstr pbs