diff --git a/src/kernel_services/ast_queries/logic_utils.ml b/src/kernel_services/ast_queries/logic_utils.ml index c79a9d15400378bf7b19ef8e81b76a91867a118c..b3fa33f9651f562c46c75675870e2bdbe52f198e 100644 --- a/src/kernel_services/ast_queries/logic_utils.ml +++ b/src/kernel_services/ast_queries/logic_utils.ml @@ -394,7 +394,8 @@ let is_boolean_binop op = let float_builtin prefix fkind = let name = match fkind with | FFloat -> Printf.sprintf "\\%s_float" prefix - | FDouble | FLongDouble -> Printf.sprintf "\\%s_double" prefix + | FDouble -> Printf.sprintf "\\%s_double" prefix + | FLongDouble -> Kernel.not_yet_implemented "Builtins for long double type" in match Logic_env.find_all_logic_functions name with | [ lf ] -> Some lf | _ -> Kernel.fatal "Missing or ambiguous builtin %S" name