diff --git a/configure.in b/configure.in
index bd80410d9aaabce56d487142e6068393de37b9c3..60f6dab2a2ca8ded43f37965ef3c099e0b52e3d8 100644
--- a/configure.in
+++ b/configure.in
@@ -396,9 +396,9 @@ AC_ARG_ENABLE(
   ENABLE_LANDMARKS=yes)
 
 if test "$ENABLE_LANDMARKS" = yes ; then
-  AC_MSG_CHECKING(for Landmarks)
+  AC_MSG_CHECKING(for Landmarks and Landmarks-ppx)
   LANDMARKS_PATH=$($OCAMLFIND query landmarks 2>/dev/null | tr -d '\r\n')
-  LANDMARKS_PPX_PATH=$($OCAMLFIND query landmarks.ppx 2>/dev/null | tr -d '\r\n')
+  LANDMARKS_PPX_PATH=$($OCAMLFIND query landmarks-ppx 2>/dev/null | tr -d '\r\n')
   if test -f "$LANDMARKS_PATH/landmark.$DYN_SUFFIX" -a -f "$LANDMARKS_PPX_PATH/ppx_landmarks.$DYN_SUFFIX"; then
     HAS_LANDMARKS="yes";
     AC_MSG_RESULT(found)
diff --git a/share/Makefile.config.in b/share/Makefile.config.in
index 06e6dd9f0258ec6ced459a3dbd65db26fbd65346..464201745d7a863b563fc672e249b8649b479237 100644
--- a/share/Makefile.config.in
+++ b/share/Makefile.config.in
@@ -200,7 +200,7 @@ LIBRARY_NAMES := \
   findlib ocamlgraph unix str dynlink bytes zarith yojson bigarray
 
 ifeq ($(HAS_LANDMARKS),yes)
-LIBRARY_NAMES += landmarks landmarks.ppx
+LIBRARY_NAMES += landmarks landmarks-ppx
 endif
 
 ifneq ($(ENABLE_GUI),no)
diff --git a/src/plugins/dive/build.ml b/src/plugins/dive/build.ml
index 5ed33280abbfe89e3c1eff6b08f1889e92208105..6a08979f28db393ec3fcb6024a20c670f6a89241 100644
--- a/src/plugins/dive/build.ml
+++ b/src/plugins/dive/build.ml
@@ -47,7 +47,7 @@ struct
   let visitor f =
     object
       inherit Visitor.frama_c_inplace
-      method! vlval lval = f lval; SkipChildren
+      method! vlval lval = f lval; Cil.SkipChildren
     end
 
   let from_exp f exp =
diff --git a/src/plugins/wp/TacInduction.ml b/src/plugins/wp/TacInduction.ml
index 982d6e13094975ab7f745b627379946d953b1b53..4098efd7c3ab847edd4ddd45b1cc5adc985493fd 100644
--- a/src/plugins/wp/TacInduction.ml
+++ b/src/plugins/wp/TacInduction.ml
@@ -108,7 +108,7 @@ class induction =
       let value = Tactical.selected s in
       if F.is_int value then
         match self#get_base () with
-        | Some base -> Applicable(process value base)
+        | Some base -> Tactical.Applicable(process value base)
         | None -> Not_configured
       else Not_applicable
 
diff --git a/src/plugins/wp/TacSequence.ml b/src/plugins/wp/TacSequence.ml
index 8a0dbdeea4cef4a56eb85356d71d4a0f2732fbbf..3671cd67b73db65cf679ea358e3a6b56640dba10 100644
--- a/src/plugins/wp/TacSequence.ml
+++ b/src/plugins/wp/TacSequence.ml
@@ -59,7 +59,7 @@ class sequence =
       | Fun(f,[a;n]) when f == Vlist.f_repeat ->
           let result = F.typeof value in
           let at = Tactical.at s in
-          Applicable
+          Tactical.Applicable
             begin
               match self#get_field vmode with
               | `Sum ->