diff options
| -rw-r--r-- | plugins/firstorder/g_ground.mlg | 14 |
1 files changed, 0 insertions, 14 deletions
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 |