diff options
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml index 5d127f6d..42ba254e 100644 --- a/src/pretty_print_lem.ml +++ b/src/pretty_print_lem.ml @@ -1210,7 +1210,8 @@ let doc_mutrec_lem = function let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) = match fcls with | [] -> failwith "FD_function with empty function list" - | FCL_aux (FCL_Funcl(id,_),_) :: _ + (* TODO: Move splitting of execute function to the rewriter *) + (*| FCL_aux (FCL_Funcl(id,_),_) :: _ when string_of_id id = "execute" (*|| string_of_id id = "initial_analysis"*) -> let (_,auxiliary_functions,clauses) = List.fold_left @@ -1273,7 +1274,7 @@ let rec doc_fundef_lem (FD_aux(FD_function(r, typa, efa, fcls),fannot) as fd) = auxiliary_functions ^^ hardline ^^ hardline ^^ (prefix 2 1) ((separate space) [string "let" ^^ doc_rec_lem false r ^^ doc_id_lem id;equals;string "function"]) - (clauses ^/^ string "end") + (clauses ^/^ string "end")*) | FCL_aux (FCL_Funcl(id,_),annot) :: _ when not (Env.is_extern id (env_of_annot annot) "lem") -> string "let" ^^ (doc_rec_lem (List.length fcls > 1) r) ^^ (doc_fundef_rhs_lem fd) |