diff options
| author | Gaëtan Gilbert | 2020-10-09 21:51:12 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-10-26 14:41:39 +0100 |
| commit | 5146b2f01b3b901ac99823d3a448c77560f248db (patch) | |
| tree | 135ce50f8d5ff9cc24e7101ca3b0c2cecb4da182 /plugins | |
| parent | 9e7b0f9f248a1fae8e5681815bd621f182696c4f (diff) | |
Improve tactic interpreter registration API a bit
Using it feels nicer this way, with GADT details hidden inside comtactic
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/ltac/g_ltac.mlg | 4 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 2 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.mli | 2 |
3 files changed, 4 insertions, 4 deletions
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index 6cf5d30a95..2d74323689 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -402,7 +402,7 @@ VERNAC { tactic_mode } EXTEND VernacSolve STATE proof { classify_as_proofstep } -> { let g = Option.default (Goal_select.get_default_goal_selector ()) g in let global = match g with Goal_select.SelectAll | Goal_select.SelectList _ -> true | _ -> false in - let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global; ast = t; }) in + let t = Tacinterp.hide_interp { Tacinterp.global; ast = t; } in ComTactic.solve g ~info t ~with_end_tac } END @@ -415,7 +415,7 @@ VERNAC { tactic_mode } EXTEND VernacSolveParallel STATE proof VtProofStep{ proof_block_detection = pbr } } -> { let t, abstract = rm_abstract t in - let t = ComTactic.I (Tacinterp.hide_interp, { Tacinterp.global = true; ast = t; }) in + let t = Tacinterp.hide_interp { Tacinterp.global = true; ast = t; } in ComTactic.solve_parallel ~info t ~abstract ~with_end_tac } END diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 12bfb4d09e..22b9abda20 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -2019,7 +2019,7 @@ let hide_interp {global;ast} = hide_interp (Proofview.Goal.env gl) end -let hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp +let ComTactic.Interpreter hide_interp = ComTactic.register_tactic_interpreter "ltac1" hide_interp (***************************************************************************) (** Register standard arguments *) diff --git a/plugins/ltac/tacinterp.mli b/plugins/ltac/tacinterp.mli index 01d7306c9d..dba9c938ec 100644 --- a/plugins/ltac/tacinterp.mli +++ b/plugins/ltac/tacinterp.mli @@ -131,7 +131,7 @@ type tactic_expr = { ast: Tacexpr.raw_tactic_expr; } -val hide_interp : tactic_expr ComTactic.tactic_interpreter +val hide_interp : tactic_expr -> ComTactic.interpretable (** Internals that can be useful for syntax extensions. *) |