aboutsummaryrefslogtreecommitdiffhomepage
path: root/engine/termops.ml
diff options
context:
space:
mode:
Diffstat (limited to 'engine/termops.ml')
-rw-r--r--engine/termops.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/engine/termops.ml b/engine/termops.ml
index b7fa2dc4a..0f84d7868 100644
--- a/engine/termops.ml
+++ b/engine/termops.ml
@@ -327,11 +327,11 @@ let pr_evar_constraints sigma pbs =
Namegen.make_all_name_different env sigma
in
print_env_short env ++ spc () ++ str "|-" ++ spc () ++
- print_constr_env env sigma (EConstr.of_constr t1) ++ spc () ++
+ protect (print_constr_env env sigma) (EConstr.of_constr t1) ++ spc () ++
str (match pbty with
| Reduction.CONV -> "=="
| Reduction.CUMUL -> "<=") ++
- spc () ++ print_constr_env env Evd.empty (EConstr.of_constr t2)
+ spc () ++ protect (print_constr_env env Evd.empty) (EConstr.of_constr t2)
in
prlist_with_sep fnl pr_evconstr pbs