Revision dccec723
Added by LĂ©lio Brun over 3 years ago
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
a version that almost work for the k-inuctive two_counters example