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/printers.ml
581 581
    fprintf fmt "@[<hov 2>(*@contract@ ";
582 582
    pp_spec fmt c;
583 583
    fprintf fmt "@]*)@ "
584
  | NodeSpec (name, _) ->
584
  | NodeSpec name ->
585 585
    (* Pushing stmts in contract. We update the original information with the
586 586
       computed one in nd. *)
587 587
    let pp_l = pp_comma_list pp_var_name in

Also available in: Unified diff