diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index 4596f23f..27484560 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1775,6 +1775,10 @@ let doc_exp, doc_let = | E_aux (E_if (c', t', e'), _) | E_aux (E_cast (_, E_aux (E_if (c', t', e'), _)), _) -> if_exp ctxt true c' t' e' + (* Special case to prevent current arm decoder becoming a staircase *) + (* TODO: replace with smarter pretty printing *) + | E_aux (E_internal_plet (pat,exp1,E_aux (E_cast (typ, (E_aux (E_if (_, _, _), _) as exp2)),_)),ann) when Typ.compare typ unit_typ == 0 -> + string "else" ^/^ top_exp ctxt false (E_aux (E_internal_plet (pat,exp1,exp2),ann)) | _ -> prefix 2 1 (string "else") (top_exp ctxt false e) in (prefix 2 1 |