aboutsummaryrefslogtreecommitdiff
path: root/ltac/rewrite.mli
diff options
context:
space:
mode:
Diffstat (limited to 'ltac/rewrite.mli')
-rw-r--r--ltac/rewrite.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/rewrite.mli b/ltac/rewrite.mli
index 35c4483513..bf56eec10e 100644
--- a/ltac/rewrite.mli
+++ b/ltac/rewrite.mli
@@ -105,7 +105,7 @@ val setoid_symmetry_in : Id.t -> unit Proofview.tactic
val setoid_reflexivity : unit Proofview.tactic
-val setoid_transitivity : constr option -> unit Proofview.tactic
+val setoid_transitivity : EConstr.constr option -> unit Proofview.tactic
val apply_strategy :