aboutsummaryrefslogtreecommitdiff
path: root/tactics/tactics.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tactics.mli')
-rw-r--r--tactics/tactics.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 084aba9efa..1c64e47e84 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -338,3 +338,6 @@ val tclABSTRACT : identifier option -> tactic -> tactic
val admit_as_an_axiom : tactic
val abstract_generalize : identifier -> tactic
+
+val register_general_multi_rewrite :
+ (bool -> evars_flag -> constr with_ebindings -> clause -> tactic) -> unit