From ef61bb05911d19c77d565d78dc57107d40c333e4 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 24 Jan 2015 11:54:00 +0100
Subject: Isolate a function for printing evar sets.

---
 printing/printer.ml  | 10 ++++++++++
 printing/printer.mli |  2 ++
 2 files changed, 12 insertions(+)

(limited to 'printing')

diff --git a/printing/printer.ml b/printing/printer.ml
index 3403fb9c3b..8a2d6e7bd1 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -446,6 +446,16 @@ let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ i
 
 let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs)
 
+(* Display a list of evars given by their name, with a prefix *)
+let pr_ne_evar_set hd tl sigma l =
+  if l != Evar.Set.empty then
+    let l = Evar.Set.fold (fun ev ->
+      Evar.Map.add ev (Evarutil.nf_evar_info sigma (Evd.find sigma ev)))
+      l Evar.Map.empty in
+    hd ++ pr_evars sigma l ++ tl
+  else
+    mt ()
+
 let default_pr_subgoal n sigma =
   let rec prrec p = function
     | [] -> error "No such goal."
diff --git a/printing/printer.mli b/printing/printer.mli
index 6b9c70815d..42ed2b6d9e 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -137,6 +137,8 @@ val pr_nth_open_subgoal    : int -> std_ppcmds
 val pr_evar                : evar_map -> (evar * evar_info) -> std_ppcmds
 val pr_evars_int           : evar_map -> int -> evar_info Evar.Map.t -> std_ppcmds
 val pr_evars               : evar_map -> evar_info Evar.Map.t -> std_ppcmds
+val pr_ne_evar_set         : std_ppcmds -> std_ppcmds -> evar_map ->
+  Evar.Set.t -> std_ppcmds
 
 val pr_prim_rule           : prim_rule -> std_ppcmds
 
-- 
cgit v1.2.3