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 ->