aboutsummaryrefslogtreecommitdiff
path: root/plugins/cc
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/cc')
-rw-r--r--plugins/cc/ccalgo.ml1
1 files changed, 0 insertions, 1 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index fdc70ccaa8..f9078c4bdc 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -33,7 +33,6 @@ let debug x =
let () =
let gdopt=
{ optdepr=false;
- optname="Congruence Verbose";
optkey=["Congruence";"Verbose"];
optread=(fun ()-> !cc_verbose);
optwrite=(fun b -> cc_verbose := b)}