diff options
| author | Thomas Bauereiss | 2018-04-18 16:04:59 +0100 |
|---|---|---|
| committer | Thomas Bauereiss | 2018-04-18 16:04:59 +0100 |
| commit | 9c25bec8e6106e1888719646867cccb24d71ca4a (patch) | |
| tree | d1302cc84efeddc2cdc31eb62d302bb95583d69b | |
| parent | e1b2379f9058e858722f2bd9691c76d00c00dcaa (diff) | |
Fix bug in pretty-printing loops to Lem
| -rw-r--r-- | src/pretty_print_lem.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 025e876e..15cd0512 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -634,6 +634,10 @@ let doc_exp_lem, doc_let_lem = let loopvar, body = match body with | E_aux (E_let (LB_aux (LB_val ( P_aux (P_typ (_, P_aux (P_var (P_aux (P_id id, _), _), _)), _), _), _), body), _) -> id, body + | E_aux (E_let (LB_aux (LB_val ( + P_aux (P_var (P_aux (P_id id, _), _), _), _), _), body), _) -> id, body + | E_aux (E_let (LB_aux (LB_val ( + P_aux (P_id id, _), _), _), body), _) -> id, body | _ -> raise (Reporting_basic.err_unreachable l ("Unable to find loop variable in " ^ string_of_exp body)) in let step = match ord_exp with | E_aux (E_lit (L_aux (L_false, _)), _) -> |