diff options
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/g_ground.mlg | 2 | ||||
| -rw-r--r-- | plugins/firstorder/ground.ml | 12 |
2 files changed, 7 insertions, 7 deletions
diff --git a/plugins/firstorder/g_ground.mlg b/plugins/firstorder/g_ground.mlg index 1128a78093..a212d13453 100644 --- a/plugins/firstorder/g_ground.mlg +++ b/plugins/firstorder/g_ground.mlg @@ -66,7 +66,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.tag (entry, [])) + Tacexpr.TacML (CAst.make (entry, [])) let (set_default_solver, default_solver, print_default_solver) = Tactic_option.declare_tactic_option ~default:default_intuition_tac "Firstorder default solver" diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 516b04ea21..6a80525200 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -18,16 +18,16 @@ open Tacticals.New open Globnames let update_flags ()= - let f acc coe = - match coe.Classops.coe_value with - | ConstRef c -> Names.Cpred.add c acc - | _ -> acc + let open TransparentState in + let f accu coe = match coe.Classops.coe_value with + | ConstRef kn -> { accu with tr_cst = Names.Cpred.remove kn accu.tr_cst } + | _ -> accu in - let pred = List.fold_left f Names.Cpred.empty (Classops.coercions ()) in + let flags = List.fold_left f TransparentState.full (Classops.coercions ()) in red_flags:= CClosure.RedFlags.red_add_transparent CClosure.betaiotazeta - (Names.Id.Pred.full,Names.Cpred.complement pred) + flags let ground_tac solver startseq = Proofview.Goal.enter begin fun gl -> |