Project

General

Profile

Revision dda9eb32 src/backends/Ada/ada_backend_ads.ml

View differences:

src/backends/Ada/ada_backend_ads.ml
107 107
  match opt_contract with
108 108
    | None -> pp_prototype fmt
109 109
    | Some contract -> 
110
        fprintf fmt "@[<v 2>%t with@,%a,@,%a@]"
110
        fprintf fmt "@[<v 2>%t with@,%a%t%a@]"
111 111
          pp_prototype
112 112
          (Utils.fprintf_list ~sep:",@," pp_pre) contract.assume
113
          (Utils.pp_final_char_if_non_empty ",@," contract.assume)
113 114
          (Utils.fprintf_list ~sep:",@," pp_post) contract.guarantees
114 115

  
115 116
(** Print the prototype with a contract of the reset procedure from a machine.

Also available in: Unified diff