diff --git a/src/plugins/wp/Factory.ml b/src/plugins/wp/Factory.ml index 5b9e54a4366c72f7bb67221e95d61d953d510e98..3fde0d76ebc9cc5324d2e3f06993c4a0734bb00c 100644 --- a/src/plugins/wp/Factory.ml +++ b/src/plugins/wp/Factory.ml @@ -242,7 +242,7 @@ module MakeCompiler(M:Sigs.Model) = struct module M = M module C = CodeSemantics.Make(M) module L = LogicSemantics.Make(M) - module A = LogicAssigns.Make(M)(C)(L) + module A = LogicAssigns.Make(M)(L) end module Comp_Region = MakeCompiler(Register(Static)(MemRegion)) diff --git a/src/plugins/wp/LogicAssigns.ml b/src/plugins/wp/LogicAssigns.ml index 8da52bbfe3284f24683773458023027af7e55c15..fe9eab80a7ce01c0d132c125dd09933c64dd5eb1 100644 --- a/src/plugins/wp/LogicAssigns.ml +++ b/src/plugins/wp/LogicAssigns.ml @@ -24,7 +24,6 @@ open Sigs module Make ( M : Sigs.Model ) - ( C : Sigs.CodeSemantics with module M = M ) ( L : Sigs.LogicSemantics with module M = M ) = struct diff --git a/src/plugins/wp/LogicAssigns.mli b/src/plugins/wp/LogicAssigns.mli index 92cd1d2006bb61cfbbe5f75ab8966db08f01d1c2..4ff9a6fb815eacb80e9e16244001a60062392260 100644 --- a/src/plugins/wp/LogicAssigns.mli +++ b/src/plugins/wp/LogicAssigns.mli @@ -22,6 +22,5 @@ module Make ( M : Sigs.Model ) - ( C : Sigs.CodeSemantics with module M = M ) ( L : Sigs.LogicSemantics with module M = M ) : Sigs.LogicAssigns with module M = M and module L = L