diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/ocaml_backend.ml | 2 | ||||
| -rw-r--r-- | src/rewrites.ml | 2 |
2 files changed, 3 insertions, 1 deletions
diff --git a/src/ocaml_backend.ml b/src/ocaml_backend.ml index c535554b..c94c0a0b 100644 --- a/src/ocaml_backend.ml +++ b/src/ocaml_backend.ml @@ -587,6 +587,8 @@ let nf_group doc = let ocaml_def ctx def = match def with | DEF_reg_dec ds -> nf_group (ocaml_dec_spec ctx ds) ^^ ocaml_def_end | DEF_fundef fd -> group (ocaml_fundef ctx fd) ^^ twice hardline + | DEF_internal_mutrec fds -> + separate_map (twice hardline) (fun fd -> group (ocaml_fundef ctx fd)) fds ^^ twice hardline | DEF_type td -> nf_group (ocaml_typedef ctx td) ^^ ocaml_def_end | DEF_val lb -> nf_group (string "let" ^^ space ^^ ocaml_letbind ctx lb) ^^ ocaml_def_end | _ -> empty diff --git a/src/rewrites.ml b/src/rewrites.ml index 06e0934f..462cbb25 100644 --- a/src/rewrites.ml +++ b/src/rewrites.ml @@ -2980,7 +2980,6 @@ let rewrite_defs_lem = [ ] let rewrite_defs_ocaml = [ - (* ("top_sort_defs", top_sort_defs); *) (* ("undefined", rewrite_undefined); *) ("no_effect_check", (fun defs -> opt_no_effects := true; defs)); ("pat_lits", rewrite_defs_pat_lits); @@ -2990,6 +2989,7 @@ let rewrite_defs_ocaml = [ ("remove_vector_concat", rewrite_defs_remove_vector_concat); ("remove_bitvector_pats", rewrite_defs_remove_bitvector_pats); ("exp_lift_assign", rewrite_defs_exp_lift_assign); + ("top_sort_defs", top_sort_defs); ("constraint", rewrite_constraint); ("trivial_sizeof", rewrite_trivial_sizeof); ("sizeof", rewrite_sizeof); |