diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-04-13 13:44:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-04-14 08:59:36 +0200 |
| commit | dc29a85d428d95fa3a3b1d30373f353436bf04a9 (patch) | |
| tree | d8315023eebd992e461bf6d14796006171f486a3 /tactics/hints.mli | |
| parent | 7f49f829260078f76c5b219472afb4fa1abce5f9 (diff) | |
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.
Diffstat (limited to 'tactics/hints.mli')
| -rw-r--r-- | tactics/hints.mli | 15 |
1 files changed, 12 insertions, 3 deletions
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 |