From 30746e6a9a3296c1aacb2fc03e1c16014232219f Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Tue, 21 Nov 2017 16:42:42 +0100 Subject: Deprecate dead code option Congruence Depth. --- plugins/firstorder/g_ground.ml4 | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/firstorder') 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 -- cgit v1.2.3