From 27fcfb54888155ceb3da3a9966e9764c0b68055d Mon Sep 17 00:00:00 2001
From: Gabriel Kerneis
Date: Sat, 7 Jun 2014 09:15:06 +0100
Subject: Print holes as [x]

---
 src/lem_interp/pretty_interp.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src')

diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 7740b149..f14a7ce1 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -4,6 +4,7 @@
  * - string_of_big_int instead of string_of_int
  * - annot does not contain type annotations anymore, so E_internal_cast
  *   is ignored
+ * - special case for holes in doc_id
  * - pp_exp returns a string instead of working on a buffer (should
  *   change this in the original as well, probably)
  * - pp_defs deleted
@@ -26,6 +27,7 @@ open PPrint
 
 let doc_id (Id_aux(i,_)) =
   match i with
+  | Id "0" -> string "[x]" (* internal representation of a hole *)
   | Id i -> string i
   | DeIid x ->
       (* add an extra space through empty to avoid a closing-comment
-- 
cgit v1.2.3