diff --git a/src/plugins/wp/Generator.ml b/src/plugins/wp/Generator.ml index 2af03b61f95049479258ddd16bec9713d7ef2f2b..28ffe5d62128f381219d524760d8db09c648547c 100644 --- a/src/plugins/wp/Generator.ml +++ b/src/plugins/wp/Generator.ml @@ -64,7 +64,7 @@ let create () : Wpo.generator = let default f = function Some v -> v | None -> f () in let dump = default Wp_parameters.Dump.get dump in - let legacy = default Wp_parameters.Dump.get legacy in + let legacy = default Wp_parameters.Legacy.get legacy in let driver = default Driver.load_driver driver in let setup = default user_setup setup in if legacy then diff --git a/src/plugins/wp/Generator.mli b/src/plugins/wp/Generator.mli index fc70c5d2fed6f9d4361d3f53313b271b5dcd990e..ef3b2b2dcee2e94f35251f971a83798e795bf564 100644 --- a/src/plugins/wp/Generator.mli +++ b/src/plugins/wp/Generator.mli @@ -20,9 +20,6 @@ (* *) (*****************************************t*********************************) -open Cil_types -open Wp_parameters - (* -------------------------------------------------------------------------- *) (* --- WP Computer (main entry points) --- *) (* -------------------------------------------------------------------------- *)