diff options
| author | Pierre-Marie Pédrot | 2019-11-29 11:53:02 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-11-29 11:53:02 +0100 |
| commit | 59656b1380a1feba954d1f32e02bb70cd548ca75 (patch) | |
| tree | 1ec23a1cccaef0b95e6f629a1694e448df8b7fbb /plugins | |
| parent | fc5fa8ffafcb0c1e3e0afcc414dfa14f7c85b6d7 (diff) | |
| parent | b1cb867a33adb576bffcfb209801a37c60bbba8f (diff) | |
Merge PR #11186: Remove undocumented and deprecated `Congruence Depth` option
Reviewed-by: ppedrot
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 |