diff --git a/src/kernel_services/ast_queries/logic_env.ml b/src/kernel_services/ast_queries/logic_env.ml index 9ba7c2a34f2ed8a53bad27d6c705a308836d8eda..cee9bf044d5529321e5c238e99371303e9db38a1 100644 --- a/src/kernel_services/ast_queries/logic_env.ml +++ b/src/kernel_services/ast_queries/logic_env.ml @@ -317,7 +317,7 @@ let builtin_states = [ Logic_builtin.self; Logic_type_builtin.self; Logic_ctor_builtin.self ] module Builtins= struct - include Hook.Make(struct end) + include Hook.Make() (* ensures we do not apply the hooks twice *) module Applied = State_builder.False_ref diff --git a/src/kernel_services/cmdline_parameters/cmdline.ml b/src/kernel_services/cmdline_parameters/cmdline.ml index 8e8917faa9749ef2eb6661dc5c3cf73db343f158..019989e9ef1e26ecdd7c8267668b9a04f5b22917 100644 --- a/src/kernel_services/cmdline_parameters/cmdline.ml +++ b/src/kernel_services/cmdline_parameters/cmdline.ml @@ -158,7 +158,7 @@ let protect = function (** {2 Exiting Frama-C} *) (* ************************************************************************* *) -module NormalExit = Hook.Make(struct end) +module NormalExit = Hook.Make() let at_normal_exit = NormalExit.extend let run_normal_exit_hook = NormalExit.apply @@ -617,7 +617,7 @@ struct let nb_actions = ref 0 let is_going_to_run () = incr nb_actions - module H = Hook.Make(struct end) + module H = Hook.Make() let () = H.extend Log.treat_deferred_error diff --git a/src/kernel_services/plugin_entry_points/db.ml b/src/kernel_services/plugin_entry_points/db.ml index 69383faea0bdae2dd7329a0d55062024fac86df0..76c8222d724d27a819828530e4510964c0f8bd99 100644 --- a/src/kernel_services/plugin_entry_points/db.ml +++ b/src/kernel_services/plugin_entry_points/db.ml @@ -37,7 +37,7 @@ let register_guarded_compute is_computed r f = r := compute module Main = struct - include Hook.Make(struct end) + include Hook.Make() let play = mk_fun "Main.play" end diff --git a/src/libraries/project/project.ml b/src/libraries/project/project.ml index c0acfdff8947452331f840db6117e8ade36a124b..c2be72957be9a316bc382208c028fb7adb99e5c8 100644 --- a/src/libraries/project/project.ml +++ b/src/libraries/project/project.ml @@ -435,13 +435,13 @@ let clear_all () = exception IOError = Sys_error -module Before_load = Hook.Make(struct end) +module Before_load = Hook.Make() let register_before_load_hook = Before_load.extend -module After_load = Hook.Make(struct end) +module After_load = Hook.Make() let register_after_load_hook = After_load.extend -module After_global_load = Hook.Make(struct end) +module After_global_load = Hook.Make() let register_after_global_load_hook = After_global_load.extend let magic = 9 (* magic number *) diff --git a/src/plugins/e-acsl/src/libraries/gmp_types.ml b/src/plugins/e-acsl/src/libraries/gmp_types.ml index 9e23d23a5d478b7bd2e6e590a37a2691f83143d4..965406bdc339c1d6e6260f46ff971452e4f58e83 100644 --- a/src/plugins/e-acsl/src/libraries/gmp_types.ml +++ b/src/plugins/e-acsl/src/libraries/gmp_types.ml @@ -76,8 +76,8 @@ module Make() = struct end -module Z = Make(struct end) -module Q = Make(struct end) +module Z = Make() +module Q = Make() let bitcnt_type_info_ref = mk_dummy_type_info_ref () diff --git a/src/plugins/gui/gtk_helper.ml b/src/plugins/gui/gtk_helper.ml index 7ca273c4caa42910c0f3909f27ce949ff3eaadcf..20df4ae960110acfb74801ce47b078f327453203 100644 --- a/src/plugins/gui/gtk_helper.ml +++ b/src/plugins/gui/gtk_helper.ml @@ -287,7 +287,7 @@ module Lock = struct end module Unlock = struct let first = ref (fun () -> ()) - module H = Hook.Make(struct end) + module H = Hook.Make() let extend is_first f = if is_first then first := f else H.extend f let apply () = !first (); H.apply () end diff --git a/src/plugins/gui/launcher.ml b/src/plugins/gui/launcher.ml index 138bce2502e143f5098ed3a6d3b149f8f7e22952..e6d9dbf1fb4883606dc28c0c1faea373ba7978c9 100644 --- a/src/plugins/gui/launcher.ml +++ b/src/plugins/gui/launcher.ml @@ -22,7 +22,7 @@ open Gtk_helper -module Kernel_hook = Hook.Make(struct end) +module Kernel_hook = Hook.Make() class type basic_main = object inherit host