diff options
| author | Maxime Dénès | 2019-07-25 18:42:09 +0200 |
|---|---|---|
| committer | Théo Zimmermann | 2019-11-26 11:37:54 +0100 |
| commit | b1cb867a33adb576bffcfb209801a37c60bbba8f (patch) | |
| tree | 48ce4456e9b9628e0ed70fe2b19b38f1a8d2bdd6 /plugins | |
| parent | 669075119cc0ea8e495a83668fad4f6c1e4f5968 (diff) | |
Remove undocumented and deprecated `Congruence Depth` option
It was a no-op.
Diffstat (limited to 'plugins')
| -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 |