From b1cb867a33adb576bffcfb209801a37c60bbba8f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 25 Jul 2019 18:42:09 +0200
Subject: Remove undocumented and deprecated `Congruence Depth` option

It was a no-op.
---
 plugins/firstorder/g_ground.mlg | 14 --------------
 1 file changed, 14 deletions(-)

(limited to 'plugins')

diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg
index 2bc79d45d4..8946587a02 100644
--- a/plugins/firstorder/g_ground.mlg
+++ b/plugins/firstorder/g_ground.mlg
@@ -47,20 +47,6 @@ let ()=
     declare_int_option gdopt
 
 
-let ()=
-  let congruence_depth=ref 100 in
-  let gdopt=
-    { optdepr=true; (* noop *)
-      optname="Congruence Depth";
-      optkey=["Congruence";"Depth"];
-      optread=(fun ()->Some !congruence_depth);
-      optwrite=
-   (function
-        None->congruence_depth:=0
-      |	Some i->congruence_depth:=(max i 0))}
-  in
-    declare_int_option gdopt
-
 let default_intuition_tac =
   let tac _ _ = Auto.h_auto None [] None in
   let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in
-- 
cgit v1.2.3