Skip to content
Snippets Groups Projects
Commit dda9eb32 authored by Guillaume DAVY's avatar Guillaume DAVY
Browse files

Ada: Correct contract printing

parent 83f4b59c
No related branches found
No related tags found
No related merge requests found
...@@ -107,9 +107,10 @@ let pp_procedure_prototype_contract pp_prototype fmt opt_contract = ...@@ -107,9 +107,10 @@ let pp_procedure_prototype_contract pp_prototype fmt opt_contract =
match opt_contract with match opt_contract with
| None -> pp_prototype fmt | None -> pp_prototype fmt
| Some contract -> | Some contract ->
fprintf fmt "@[<v 2>%t with@,%a,@,%a@]" fprintf fmt "@[<v 2>%t with@,%a%t%a@]"
pp_prototype pp_prototype
(Utils.fprintf_list ~sep:",@," pp_pre) contract.assume (Utils.fprintf_list ~sep:",@," pp_pre) contract.assume
(Utils.pp_final_char_if_non_empty ",@," contract.assume)
(Utils.fprintf_list ~sep:",@," pp_post) contract.guarantees (Utils.fprintf_list ~sep:",@," pp_post) contract.guarantees
(** Print the prototype with a contract of the reset procedure from a machine. (** Print the prototype with a contract of the reset procedure from a machine.
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment