From 90f0778f6512312784ef21c8621cf69f2e8764eb Mon Sep 17 00:00:00 2001
From: Andre Maroneze <andre.oliveiramaroneze@cea.fr>
Date: Fri, 15 Feb 2019 11:48:04 +0100
Subject: [PATCH] [ocaml] silence spurious warnings about partial applications
---
src/plugins/metrics/register_gui.ml | 7 ++++---
src/plugins/occurrence/register_gui.ml | 4 ++--
src/plugins/rte/register.ml | 8 ++++----
src/plugins/wp/TacShift.ml | 2 +-
src/plugins/wp/register.ml | 2 +-
src/plugins/wp/wpo.ml | 2 +-
6 files changed, 13 insertions(+), 12 deletions(-)
diff --git a/src/plugins/metrics/register_gui.ml b/src/plugins/metrics/register_gui.ml
index f16d7007a7d..38cb84cfccd 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 9fbba556725..3df2230eeac 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 ab0d3111c0a..99e58a483d2 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 fff37a69094..4a1d714fa8c 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 b8bbb65f08b..33157b91821 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 b4ff5124a5c..782b9a5425d 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
--
GitLab