diff options
| author | Emilio Jesus Gallego Arias | 2018-11-05 02:51:23 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-11-17 05:29:50 +0100 |
| commit | 4949b991019dd6dd845627cc03e800072bc7ed10 (patch) | |
| tree | 6d77ed011a33e2afdcd544ff301aa84a2056f9d2 /plugins/firstorder | |
| parent | f8a76b3d383abf468fb21df509f5da8f8aafa913 (diff) | |
[ltac] Use CAst nodes in the tactic AST.
This provides several advantages to people serializing tactic
scripts. Appearance of the involved constructors is common enough as
to bother to submit this PR.
Diffstat (limited to 'plugins/firstorder')
| -rw-r--r-- | plugins/firstorder/g_ground.mlg | 2 |
1 files changed, 1 insertions, 1 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" |