diff options
Diffstat (limited to 'tactics/dhyp.mli')
| -rw-r--r-- | tactics/dhyp.mli | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli index 4879bafc7..bedbb26c9 100644 --- a/tactics/dhyp.mli +++ b/tactics/dhyp.mli @@ -15,5 +15,16 @@ open Tacmach (* Programmable destruction of hypotheses and conclusions. *) +val set_extern_interp : (Tacexpr.raw_tactic_expr -> tactic) -> unit + +(* val dHyp : identifier -> tactic val dConcl : tactic +*) +val h_destructHyp : bool -> identifier -> tactic +val h_destructConcl : tactic +val h_auto_tdb : int option -> tactic + +val add_destructor_hint : + identifier -> (bool,unit) Tacexpr.location -> + Genarg.constr_ast -> int -> Tacexpr.raw_tactic_expr -> unit |