diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/pretty_print_coq.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/pretty_print_coq.ml b/src/pretty_print_coq.ml index dc0b5036..9cc85601 100644 --- a/src/pretty_print_coq.ml +++ b/src/pretty_print_coq.ml @@ -1149,7 +1149,7 @@ let doc_exp_lem, doc_let_lem = if aexp_needed then parens (align epp) else align epp | E_exit e -> liftR (separate space [string "exit"; expY e]) | E_assert (e1,e2) -> - let epp = liftR (separate space [string "assert_exp"; expY e1; expY e2]) in + let epp = liftR (separate space [string "assert_exp'"; expY e1; expY e2]) in if aexp_needed then parens (align epp) else align epp | E_app_infix (e1,id,e2) -> raise (Reporting_basic.err_unreachable l @@ -1161,6 +1161,9 @@ let doc_exp_lem, doc_let_lem = let b = match e1 with E_aux (E_if _,_) -> true | _ -> false in let middle = match fst (untyp_pat pat) with + | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) + when (match e1 with E_aux (E_assert _,_) -> true | _ -> false) -> + string ">>= fun _ =>" | P_aux (P_wild,_) | P_aux (P_typ (_, P_aux (P_wild, _)), _) -> string ">>" | P_aux (P_id id,_) -> |