From dc29a85d428d95fa3a3b1d30373f353436bf04a9 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 13 Apr 2015 13:44:49 +0200 Subject: Opaque implementation of auto tactics. We provide an eliminator ensuring that the AST will be used to build a tactic, so that we can stuff arbitrary things inside. An escape function is also provided for backward compatibility. --- tactics/hints.mli | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'tactics/hints.mli') diff --git a/tactics/hints.mli b/tactics/hints.mli index 9a781c722..958cca1c3 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -28,7 +28,7 @@ val decompose_app_bound : constr -> global_reference * constr array (** Pre-created hint databases *) -type 'a auto_tactic = +type 'a auto_tactic_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) | Give_exact of 'a @@ -36,6 +36,8 @@ type 'a auto_tactic = | Unfold_nth of evaluable_global_reference (* Hint Unfold *) | Extern of Tacexpr.glob_tactic_expr (* Hint Extern *) +type 'a auto_tactic + type hints_path_atom = | PathHints of global_reference list | PathAny @@ -45,10 +47,10 @@ type 'a gen_auto_tactic = private { poly : polymorphic; (** Is the hint polymorpic and hence should be refreshed at each application *) pat : constr_pattern option; (** A pattern for the concl of the Goal *) name : hints_path_atom; (** A potential name to refer to the hint *) - code : 'a auto_tactic; (** the tactic to apply when the concl matches pat *) + code : 'a; (** the tactic to apply when the concl matches pat *) } -type pri_auto_tactic = (constr * clausenv) gen_auto_tactic +type pri_auto_tactic = (constr * clausenv) auto_tactic gen_auto_tactic type search_entry @@ -195,6 +197,13 @@ val make_extern : int -> constr_pattern option -> Tacexpr.glob_tactic_expr -> hint_entry +val run_auto_tactic : 'a auto_tactic -> + ('a auto_tactic_ast -> 'r Proofview.tactic) -> 'r Proofview.tactic + +(** This function is for backward compatibility only, not to use in newly + written code. *) +val repr_auto_tactic : 'a auto_tactic -> 'a auto_tactic_ast + val extern_intern_tac : (patvar list -> Tacexpr.raw_tactic_expr -> Tacexpr.glob_tactic_expr) Hook.t -- cgit v1.2.3