diff --git a/src/kernel_services/plugin_entry_points/kernel.ml b/src/kernel_services/plugin_entry_points/kernel.ml index ac969b3fd4a2f7b702122b6bb412fc13cb41dc26..e704803c577786149f2a0174d9f55535a104dc1b 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