diff --git a/src/kernel_services/analysis/destructors.ml b/src/kernel_services/analysis/destructors.ml index bb96f9935985e06a824e7e0e2847e76a50d0f6b3..47f549d68de9c2501a719700da277292139ba8a6 100644 --- a/src/kernel_services/analysis/destructors.ml +++ b/src/kernel_services/analysis/destructors.ml @@ -28,7 +28,11 @@ let add_destructor (_, l as acc) var = | [] -> acc | [ attr ] -> let mk_call f e args = - let kf = Globals.Functions.find_by_name f in + let kf = + try Globals.Functions.find_by_name f + with Not_found -> + Kernel.fatal "Destructor function %s does not exist" f + in let e = match Globals.Functions.get_params kf with | vi :: _ ->