Project

General

Profile

Revision 52cfee34 src/inliner.ml

View differences:

src/inliner.ml
209 209
	  let args = mkexpr loc (Expr_tuple [call_orig; call_inlined]) in 
210 210
	  mkexpr loc (Expr_appl ("=", args, None))
211 211
      }];
212
    node_dec_stateless = true;
213
    node_stateless = None;
212 214
    node_spec = Some 
213 215
      {requires = []; 
214 216
       ensures = [EnsuresExpr (mkeexpr loc (EExpr_ident ok_ident))];

Also available in: Unified diff