aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--tactics/setoid_replace.mli4
1 files changed, 3 insertions, 1 deletions
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index e41728ead5..afeb304d3f 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -32,4 +32,6 @@ val add_relation :
val add_setoid : constr_expr -> constr_expr -> constr_expr -> unit
-val new_named_morphism : Names.identifier -> constr_expr -> unit
+val new_named_morphism :
+ Names.identifier -> constr_expr -> (constr_expr list * constr_expr) option ->
+ unit