diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml index 29f760ae9ee6aec093df4f4c94a50864a65e5601..a02ddbecf0ee2978202c40d5ada24ab3d1f11295 100644 --- a/src/plugins/wp/register.ml +++ b/src/plugins/wp/register.ml @@ -748,14 +748,15 @@ let cmdline_run () = RefUsage.compute (); RefUsage.dump (); end ; - if Wp_parameters.has_dkey dkey_builtins then - begin - LogicBuiltins.dump (); - end ; let bhv = Wp_parameters.Behaviors.get () in let prop = Wp_parameters.Properties.get () in (** TODO entry point *) let computer = computer () in + if Wp_parameters.has_dkey dkey_builtins then + begin + WpContext.on_context (computer#model,WpContext.Global) + LogicBuiltins.dump (); + end ; Generator.compute_selection computer ~fct ~bhv ~prop () in match Wp_parameters.job () with