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.

---
 dev/base_include    | 1 +
 dev/top_printers.ml | 5 +++--
 2 files changed, 4 insertions(+), 2 deletions(-)

(limited to 'dev')

diff --git a/dev/base_include b/dev/base_include
index 1d43e64dfa..c2da8b18aa 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -34,6 +34,7 @@
 #install_printer  (* qualid *)  ppqualid;;
 #install_printer  (* kernel_name *) ppkn;;
 #install_printer  (* constant *) ppcon;;
+#install_printer  (* projection *) ppproj;;
 #install_printer  (* cl_index *) ppclindex;;
 #install_printer  (* recarg Rtree.t *)  ppwf_paths;;
 #install_printer  (* constr *)  print_pure_constr;;
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 1d903f30f5..75310163f3 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -43,6 +43,7 @@ let ppmbid mbid = pp (str (MBId.debug_to_string mbid))
 let ppdir dir = pp (pr_dirpath dir)
 let ppmp mp = pp(str (string_of_mp mp))
 let ppcon con = pp(debug_pr_con con)
+let ppproj con = pp(debug_pr_con (Projection.constant con))
 let ppkn kn = pp(pr_kn kn)
 let ppmind kn = pp(debug_pr_mind kn)
 let ppind (kn,i) = pp(debug_pr_mind kn ++ str"," ++int i)
@@ -146,8 +147,8 @@ let pp_state_t n = pp (Reductionops.pr_state n)
 (* proof printers *)
 let pr_evar ev = Pp.int (Evar.repr ev)
 let ppmetas metas = pp(pr_metaset metas)
-let ppevm evd = pp(pr_evar_map (Some 2) evd)
-let ppevmall evd = pp(pr_evar_map None evd)
+let ppevm evd = pp(pr_evar_map ~with_univs:!Flags.univ_print (Some 2) evd)
+let ppevmall evd = pp(pr_evar_map ~with_univs:!Flags.univ_print None evd)
 let pr_existentialset evars =
   prlist_with_sep spc pr_evar (Evar.Set.elements evars)
 let ppexistentialset evars =
-- 
cgit v1.2.3