From 8a9de08c0e6a5130103cedf05cbcebcf5f621d1e Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 8 Oct 2014 23:28:06 +0200
Subject: Add debug printers for projections, fix printing of evar constraints
 and unsatisfiable constraints which were not done in the right environment.

---
 pretyping/evd.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'pretyping')

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
 
-- 
cgit v1.2.3