Project

General

Profile

« Previous | Next » 

Revision dccec723

Added by LĂ©lio Brun over 3 years ago

a version that almost work for the k-inuctive two_counters example

View differences:

src/corelang.mli
271 271
val mk_contract_var :
272 272
  ident -> bool -> type_dec option -> expr -> Location.t -> contract_desc
273 273

  
274
val mk_contract_guarantees : string option -> eexpr -> contract_desc
274
val mk_contract_guarantees : string option -> eexpr -> proof_annotation option -> contract_desc
275 275

  
276 276
val mk_contract_assume : string option -> eexpr -> contract_desc
277 277

  

Also available in: Unified diff