aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-11-21 16:42:42 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-12-14 19:17:49 +0100
commit30746e6a9a3296c1aacb2fc03e1c16014232219f (patch)
treef3390677c41221e01cce72543f74c8984e6eec6a
parentf9b715c4ea07d6ecfece7f28e4d25f3dcab01158 (diff)
Deprecate dead code option Congruence Depth.
-rw-r--r--plugins/firstorder/g_ground.ml46
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 938bec25b..b81010c7b 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -40,17 +40,17 @@ let _=
in
declare_int_option gdopt
-let congruence_depth=ref 100
let _=
+ let congruence_depth=ref 100 in
let gdopt=
- { optdepr=false;
+ { optdepr=true; (* noop *)
optname="Congruence Depth";
optkey=["Congruence";"Depth"];
optread=(fun ()->Some !congruence_depth);
optwrite=
(function
- None->congruence_depth:=0
+ None->congruence_depth:=0
| Some i->congruence_depth:=(max i 0))}
in
declare_int_option gdopt