summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorRobert Norton2017-04-19 10:56:38 +0100
committerRobert Norton2017-04-20 11:06:05 +0100
commit20f68623e7d15493308f2da3210ad699568b5996 (patch)
tree55b229cadf4944e7864a62518b714e832c83e6ae
parentc37cbdc7916671030f2afacba351c6c0e9b3468f (diff)
support assert in ocaml shallow embedding.
-rw-r--r--src/pretty_print_ocaml.ml2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml
index 899a6caf..8f5fb591 100644
--- a/src/pretty_print_ocaml.ml
+++ b/src/pretty_print_ocaml.ml
@@ -423,6 +423,8 @@ let doc_exp_ocaml, doc_let_ocaml =
| E_internal_return (e1) ->
separate space [string "return"; exp e1;]
+ | E_assert (e1, e2) ->
+ (string "assert") ^^ parens ((string "to_bool") ^^ space ^^ exp e1) (* XXX drops e2 *)
and let_exp (LB_aux(lb,_)) = match lb with
| LB_val_explicit(ts,pat,e) ->
prefix 2 1