aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/indfun_common.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index b68b34ca35..c864bfe9f7 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -375,7 +375,7 @@ let functional_induction_rewrite_dependent_proofs_sig =
optread = (fun () -> !functional_induction_rewrite_dependent_proofs);
optwrite = (fun b -> functional_induction_rewrite_dependent_proofs := b)
}
-let _ = declare_bool_option functional_induction_rewrite_dependent_proofs_sig
+let () = declare_bool_option functional_induction_rewrite_dependent_proofs_sig
let do_rewrite_dependent () = !functional_induction_rewrite_dependent_proofs = true
@@ -388,7 +388,7 @@ let function_debug_sig =
optwrite = (fun b -> function_debug := b)
}
-let _ = declare_bool_option function_debug_sig
+let () = declare_bool_option function_debug_sig
let do_observe () = !function_debug
@@ -406,7 +406,7 @@ let strict_tcc_sig =
optwrite = (fun b -> strict_tcc := b)
}
-let _ = declare_bool_option strict_tcc_sig
+let () = declare_bool_option strict_tcc_sig
exception Building_graph of exn