diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-11-21 16:42:42 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-12-14 19:17:49 +0100 |
| commit | 30746e6a9a3296c1aacb2fc03e1c16014232219f (patch) | |
| tree | f3390677c41221e01cce72543f74c8984e6eec6a | |
| parent | f9b715c4ea07d6ecfece7f28e4d25f3dcab01158 (diff) | |
Deprecate dead code option Congruence Depth.
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 6 |
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 |