sig val compute : Kernel_function.t -> unit val is_complete : Kernel_function.t -> bool val warn : Kernel_function.t -> unit val wkey_pedantic : Wp_parameters.warn_category end