Project

General

Profile

Revision f4cba4b8 src/inliner.ml

View differences:

src/inliner.ml
421 421
    node_dec_stateless = false;
422 422
    node_stateless = None;
423 423
    node_spec = Some 
424
      (mk_contract_guarantees (mkeexpr loc (mkexpr loc (Expr_ident ok_ident))));
425
      node_annot = [];
426
  }
424
                  (Contract
425
                     (mk_contract_guarantees
426
                        (mkeexpr loc (mkexpr loc (Expr_ident ok_ident)))
427
                     )
428
                  );
429
    node_annot = [];
430
    node_iscontract = true;
431
    }
427 432
  in
428 433
  let main = [{ top_decl_desc = Node main_node; top_decl_loc = loc; top_decl_owner = filename; top_decl_itf = false }] in
429 434
  let new_prog = others@nodes_origs@nodes_inlined@main in

Also available in: Unified diff