From ddf5e988bbc87776dcc9d874867a2a1d5b511ec8 Mon Sep 17 00:00:00 2001
From: Virgile Prevosto <virgile.prevosto@cea.fr>
Date: Fri, 4 Oct 2024 14:42:59 +0200
Subject: [PATCH] [kernel] refine help msg of -inline-stmt-contracts
---
src/kernel_services/plugin_entry_points/kernel.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml
index ac969b3fd4..e704803c57 100644
--- a/src/kernel_services/plugin_entry_points/kernel.ml
+++ b/src/kernel_services/plugin_entry_points/kernel.ml
@@ -1386,7 +1386,8 @@ module InlineStmtContracts =
let option_name = "-inline-stmt-contracts"
let module_name = "InlineStmtContracts"
let help = "transforms requires/ensures clauses of statement contracts \
- into plain assertions"
+ into plain assertions, enabling their verification \
+ by plug-ins with incomplete support for statement contracts."
end)
let () = Parameter_customize.set_group normalisation
--
GitLab