From 14c8ffe6ba8b46018702c1aadfb9df72a7c80f55 Mon Sep 17 00:00:00 2001 From: Pierre Villemot Date: Fri, 22 Sep 2023 14:19:35 +0200 Subject: [PATCH] Update documentation about `output_concrete_model` I also remove the mention about the different kind of formats used to print models. Indeed, we use only the SMT-LIB format and the Why3 format is slightly different but probably outdated. --- src/lib/frontend/models.mli | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/lib/frontend/models.mli b/src/lib/frontend/models.mli index 749bed0bed..9044dd5e91 100644 --- a/src/lib/frontend/models.mli +++ b/src/lib/frontend/models.mli @@ -37,10 +37,6 @@ type t = { arrays : ModelMap.t; } -(** Print the given counterexample on the given formatter with the - corresponding format set with Options.get_output_format. - - functions: the functions of the model; - - constants: the variables of the model; - - arrays: (experimental) the arrays of the model. -*) val output_concrete_model : Format.formatter -> t -> unit +(** [output_concrete_model ppf mdl] prints the model [mdl] on + the formatter [ppf]. *)