diff options
Diffstat (limited to 'compiler/Extract.ml')
| -rw-r--r-- | compiler/Extract.ml | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/compiler/Extract.ml b/compiler/Extract.ml index 46cf8c4a..8d35f039 100644 --- a/compiler/Extract.ml +++ b/compiler/Extract.ml @@ -1475,8 +1475,6 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) *) let inputs_lvs = let all_inputs = (Option.get def.body).inputs_lvs in - (* TODO: *) - assert (not !Config.return_back_funs); let num_fwd_inputs = def.signature.fwd_info.fwd_info.num_inputs_with_fuel_with_state in @@ -1523,8 +1521,6 @@ let extract_fun_decl_gen (ctx : extraction_ctx) (fmt : F.formatter) if has_decreases_clause && !backend = Lean then ( let def_body = Option.get def.body in let all_vars = List.map (fun (v : var) -> v.id) def_body.inputs in - (* TODO: *) - assert (not !Config.return_back_funs); let num_fwd_inputs = def.signature.fwd_info.fwd_info.num_inputs_with_fuel_with_state in |