Project

General

Profile

Revision f4cba4b8 src/corelang.mli

View differences:

src/corelang.mli
58 58
val update_node: ident -> top_decl -> unit
59 59
val is_generic_node: top_decl -> bool
60 60
val is_imported_node: top_decl -> bool
61

  
61
val is_contract: top_decl -> bool
62
  
62 63
val consts_table: (ident, top_decl) Hashtbl.t
63 64
val print_consts_table:  Format.formatter -> unit -> unit
64 65
val type_table: (type_dec_desc, top_decl) Hashtbl.t
......
167 168
val mk_contract_guarantees: eexpr -> contract_desc
168 169
val mk_contract_assume: eexpr -> contract_desc
169 170
val mk_contract_mode: ident -> eexpr list -> eexpr list -> Location.t -> contract_desc
170
val mk_contract_import: ident -> expr list -> expr list -> Location.t -> contract_desc
171
val mk_contract_import: ident -> expr -> expr -> Location.t -> contract_desc
171 172
val merge_contracts:  contract_desc -> contract_desc -> contract_desc 
172 173
val extend_eexpr: (quantifier_type * var_decl list) list -> eexpr -> eexpr
173 174
val update_expr_annot: ident -> expr -> expr_annot -> expr

Also available in: Unified diff