aboutsummaryrefslogtreecommitdiff
path: root/tactics/setoid_replace.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/setoid_replace.mli')
-rw-r--r--tactics/setoid_replace.mli3
1 files changed, 3 insertions, 0 deletions
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index 3b71708b4a..4200ff5455 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -26,6 +26,9 @@ val equiv_list : unit -> constr list
val setoid_replace :
constr option -> constr -> constr -> new_goals:constr list -> tactic
+val setoid_replace_in :
+ identifier -> constr option -> constr -> constr -> new_goals:constr list ->
+ tactic
val general_s_rewrite : bool -> constr -> new_goals:constr list -> tactic
val general_s_rewrite_in :