diff --git a/src/kernel_internals/typing/infer_annotations.ml b/src/kernel_internals/typing/infer_annotations.ml index 596454178f1dc4f5f0d0bdff2797570f30e33d0a..568b2da42b83d1a254d92f98ee554bbb67209e82 100644 --- a/src/kernel_internals/typing/infer_annotations.ml +++ b/src/kernel_internals/typing/infer_annotations.ml @@ -227,7 +227,7 @@ let populate_funspec_aux kf spec = if not (is_frama_c_builtin name) then Kernel.warning ~once:true ~current:true ~wkey:Kernel.wkey_missing_spec - "No code nor %s assigns clause for function %a, \ + "Neither code nor %s assigns clause for function %a, \ generating default assigns from the %s" explicit_name Kernel_function.pretty kf orig_name in