From cfff8f8a32708ea0c8e72178424db0b40665fe37 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Fri, 17 Oct 2014 15:14:54 +0200
Subject: Experimental printing of the signature of open evars in Check.

---
 printing/printer.ml | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

(limited to 'printing/printer.ml')

diff --git a/printing/printer.ml b/printing/printer.ml
index cba33929b9..33bd5041e8 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -432,14 +432,15 @@ let pr_evar sigma (evk, evi) =
   hov 0 (pr_existential_key sigma evk ++ str " : " ++ pegl)
 
 (* Print an enumerated list of existential variables *)
-let rec pr_evars_int sigma i = function
+let rec pr_evars_int_hd head sigma i = function
   | [] -> mt ()
   | (evk,evi)::rest ->
-      (hov 0 (str "Existential " ++ int i ++ str " =" ++ spc () ++
-              pr_evar sigma (evk,evi))) ++
-      (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int sigma (i+1) rest)
+      (hov 0 (head i ++ pr_evar sigma (evk,evi))) ++
+      (match rest with [] -> mt () | _ -> fnl () ++ pr_evars_int_hd head sigma (i+1) rest)
 
-let pr_evars_int sigma i evs = pr_evars_int sigma i (Evar.Map.bindings evs)
+let pr_evars_int sigma i evs = pr_evars_int_hd (fun i -> str "Existential " ++ int i ++ str " =" ++ spc ()) sigma i (Evar.Map.bindings evs)
+
+let pr_evars sigma evs = pr_evars_int_hd (fun i -> mt ()) sigma 1 (Evar.Map.bindings evs)
 
 let default_pr_subgoal n sigma =
   let rec prrec p = function
-- 
cgit v1.2.3