diff options
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index cdc8eb375..7acd803bd 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -398,7 +398,10 @@ val general_multi_rewrite : val subst_one : (bool -> Id.t -> Id.t * constr * bool -> tactic) Hook.t + val declare_intro_decomp_eq : ((int -> tactic) -> Coqlib.coq_eq_data * types * (types * constr * constr) -> clausenv -> tactic) -> unit + +val emit_side_effects : Declareops.side_effects -> tactic |