diff options
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index b250175354..bbb9feae2e 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -30,8 +30,7 @@ let ground_depth=ref 3 let _= let gdopt= - { optsync=true; - optdepr=false; + { optdepr=false; optname="Firstorder Depth"; optkey=["Firstorder";"Depth"]; optread=(fun ()->Some !ground_depth); @@ -46,8 +45,7 @@ let congruence_depth=ref 100 let _= let gdopt= - { optsync=true; - optdepr=false; + { optdepr=false; optname="Congruence Depth"; optkey=["Congruence";"Depth"]; optread=(fun ()->Some !congruence_depth); @@ -63,7 +61,7 @@ let default_intuition_tac = let name = { Tacexpr.mltac_plugin = "ground_plugin"; mltac_tactic = "auto_with"; } in let entry = { Tacexpr.mltac_name = name; mltac_index = 0 } in Tacenv.register_ml_tactic name [| tac |]; - Tacexpr.TacML (Loc.ghost, entry, []) + Tacexpr.TacML (Loc.tag (entry, [])) let (set_default_solver, default_solver, print_default_solver) = Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver" |