diff --git a/src/plugins/metrics/register_gui.ml b/src/plugins/metrics/register_gui.ml
index f16d7007a7d889cf4c4682d7dc563ca724b6de87..38cb84cfccddc2cbce8c2403160e29125ae652e8 100644
--- a/src/plugins/metrics/register_gui.ml
+++ b/src/plugins/metrics/register_gui.ml
@@ -347,10 +347,11 @@ module ValueCoverageGUI = struct
              ~markup:(Format.sprintf "%s%% functions reached"
                         (Metrics_base.float_to_string pcent))
              ~justify:`LEFT ~packing:box#pack ());
-    let _ = Gtk_helper.on_bool box "Highlight results" (fun () -> !highlight)
-      (fun b -> highlight := b; main_ui#rehighlight ()) 
+    let _ignore = Gtk_helper.on_bool box "Highlight results"
+        (fun () -> !highlight)
+        (fun b -> highlight := b; main_ui#rehighlight ())
     in
-    let _ = Gtk_helper.on_bool box "Show columns"
+    let _ignore = Gtk_helper.on_bool box "Show columns"
         ~tooltip:"Shows the columns related to dead code in the filetree."
         (fun () -> !filetree_enabled)
         (fun b -> filetree_enabled := b; !update_filetree `Visibility)
diff --git a/src/plugins/occurrence/register_gui.ml b/src/plugins/occurrence/register_gui.ml
index 9fbba556725d43f3660638f10b1a9d21e4f993fd..3df2230eeaced7a4cf838505650b702a581205fc 100644
--- a/src/plugins/occurrence/register_gui.ml
+++ b/src/plugins/occurrence/register_gui.ml
@@ -71,7 +71,7 @@ let filter_accesses l =
         let f = consider_access () in
         List.filter (fun access -> f (Register.classify_accesses access)) l
 
-let _ =
+let _ignore =
   Dynamic.register
     ~plugin:"Occurrence"
     ~journalize:false
@@ -79,7 +79,7 @@ let _ =
     (Datatype.func Datatype.bool Datatype.unit)
     Enabled.set
 
-let _ =
+let _ignore =
   Dynamic.register
     ~plugin:"Occurrence"
     ~journalize:false
diff --git a/src/plugins/rte/register.ml b/src/plugins/rte/register.ml
index ab0d3111c0a0da3d7e9c6b7e1777e17659c14c57..99e58a483d2556e4764d4e538a57dacac76ac0b1 100644
--- a/src/plugins/rte/register.ml
+++ b/src/plugins/rte/register.ml
@@ -63,7 +63,7 @@ let journal_register ?comment is_dyn name ty_arg fctref fct =
   let ty = Datatype.func ty_arg Datatype.unit in
   Db.register (Db.Journalize("RteGen." ^ name, ty)) fctref fct;
   if is_dyn then
-    let _ =
+    let _ignore =
       Dynamic.register ?comment ~plugin:"RteGen" name ty ~journalize:true fct
     in
     ()
@@ -111,7 +111,7 @@ let _ =
 
 (* retrieve list of generated rte annotations (not precond) for
    a given stmt *)
-let _ =
+let _ignore =
   Dynamic.register
     ~comment:"Get the list of annotations previously emitted by RTE for the \
               given statement."
@@ -123,7 +123,7 @@ let _ =
     ~journalize:true
     Generator.get_registered_annotations
 
-let _ =
+let _ignore =
   Dynamic.register
     ~comment:"Generate RTE annotations corresponding to the given stmt of \
               the given function."
@@ -134,7 +134,7 @@ let _ =
     ~journalize:false
     Visit.get_annotations_stmt
 
-let _ =
+let _ignore =
   Dynamic.register
     ~comment:"Generate RTE annotations corresponding to the given exp \
               of the given stmt in the given function."
diff --git a/src/plugins/wp/TacShift.ml b/src/plugins/wp/TacShift.ml
index fff37a69094cfad98a268ab90100b7834634d576..4a1d714fa8c4f7331890a171b3ffa156a6d1289a 100644
--- a/src/plugins/wp/TacShift.ml
+++ b/src/plugins/wp/TacShift.ml
@@ -84,7 +84,7 @@ let is_shift e =
     let open Qed.Logic in
     match F.repr e with
     | Fun( f , [_;n] ) ->
-        let _ = select_op f in
+        let _ignore = select_op f in
         let _ = select_int n in
         true
     | _ -> false
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index b8bbb65f08b7cb52a063fced89af61b765c89ddc..33157b918215fb24c5a52cb16d0560e5a13744be 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -732,7 +732,7 @@ let deprecated name =
     "Dynamic '%s' now is deprecated. Use `Wp.VC` api instead." name
 
 let register name ty code =
-  let _ =
+  let _ignore =
     Dynamic.register ~plugin:"Wp" name ty
       ~journalize:false (*LC: Because of Property is not journalizable. *)
       (fun x -> deprecated name ; code x)
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index b4ff5124a5c54d708891290a466c0566b4c08f0f..782b9a5425dfb48bfc7d165900d6733b75a2b27b 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -965,7 +965,7 @@ let get_logfile w prover result =
   let model = get_model w in
   DISK.cache_log ~pid:w.po_pid ~model ~prover ~result
 
-let _ =
+let _ignore =
   Dynamic.register ~plugin:"Wp" "Wpo.file_for_log_proof" ~journalize:false
     (Datatype.func2
        WpoType.ty ProverType.ty