diff options
| author | Gabriel Kerneis | 2014-06-07 09:15:06 +0100 |
|---|---|---|
| committer | Gabriel Kerneis | 2014-06-07 09:15:06 +0100 |
| commit | 27fcfb54888155ceb3da3a9966e9764c0b68055d (patch) | |
| tree | e689fed1d2e664c7d949422afb361c02aeca88c7 /src | |
| parent | ea0d188df9884f99489d985bcaf77eb04eff10be (diff) | |
Print holes as [x]
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/pretty_interp.ml | 2 |
1 files changed, 2 insertions, 0 deletions
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 |