summaryrefslogtreecommitdiff
path: root/src/lem_interp
diff options
context:
space:
mode:
authorKathy Gray2014-11-07 16:31:03 +0000
committerKathy Gray2014-11-07 16:31:03 +0000
commit08a7d0de5e844ae8ad2d7027a4da87df054b2a28 (patch)
treef8172be5684d9fc125db382f4589f698dd1f8ca4 /src/lem_interp
parent179da2c7c29265cee601b5cb1956e18699cedd3f (diff)
stop using LEMLIB in makefile, in case that's interfering with lem library placement, switch to LEMLIBOCAML
Diffstat (limited to 'src/lem_interp')
-rw-r--r--src/lem_interp/pretty_interp.ml5
1 files changed, 4 insertions, 1 deletions
diff --git a/src/lem_interp/pretty_interp.ml b/src/lem_interp/pretty_interp.ml
index 6a72526a..b201723a 100644
--- a/src/lem_interp/pretty_interp.ml
+++ b/src/lem_interp/pretty_interp.ml
@@ -332,7 +332,10 @@ let doc_exp, doc_let =
| E_nondet exps ->
let exps_doc = separate_map (semi ^^ hardline) (exp env) exps in
string "nondet" ^^ space ^^ (surround 2 1 lbrace exps_doc rbrace)
- | E_id id -> (*TODO, use env here*) doc_id id
+ | E_id id ->
+ (match id with
+ | Id_aux(Id("0"), _) -> (*The evaluation context hole*) doc_id id
+ | _ -> doc_id id)
| E_lit lit -> doc_lit lit
| E_cast(typ,e) ->
if !ignore_casts then