aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/rewrite.mli
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac/rewrite.mli')
-rw-r--r--plugins/ltac/rewrite.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 23767c12f..63e891b45 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -110,7 +110,7 @@ val setoid_transitivity : constr option -> unit Proofview.tactic
val apply_strategy :
strategy ->
Environ.env ->
- Names.Id.t list ->
+ Names.Id.Set.t ->
constr ->
bool * constr ->
evars -> rewrite_result