aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.ml17
1 files changed, 6 insertions, 11 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 74043d6bc8..6f5c910297 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -25,19 +25,14 @@ open Util
let init_size=5
-let cc_verbose=ref false
+let cc_verbose=
+ declare_bool_option_and_ref
+ ~depr:false
+ ~key:["Congruence";"Verbose"]
+ ~value:false
let debug x =
- if !cc_verbose then Feedback.msg_debug (x ())
-
-let () =
- let gdopt=
- { optdepr=false;
- optkey=["Congruence";"Verbose"];
- optread=(fun ()-> !cc_verbose);
- optwrite=(fun b -> cc_verbose := b)}
- in
- declare_bool_option gdopt
+ if cc_verbose () then Feedback.msg_debug (x ())
(* Signature table *)