aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/rewrite.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/rewrite.mli')
-rw-r--r--tactics/rewrite.mli8
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/rewrite.mli b/tactics/rewrite.mli
index 4d1e285f9..637bab5a6 100644
--- a/tactics/rewrite.mli
+++ b/tactics/rewrite.mli
@@ -71,13 +71,13 @@ val default_morphism :
(types * constr option) option list * (types * types option) option ->
constr -> constr * constr
-val setoid_symmetry : tactic
+val setoid_symmetry : unit Proofview.tactic
-val setoid_symmetry_in : Id.t -> tactic
+val setoid_symmetry_in : Id.t -> unit Proofview.tactic
-val setoid_reflexivity : tactic
+val setoid_reflexivity : unit Proofview.tactic
-val setoid_transitivity : constr option -> tactic
+val setoid_transitivity : constr option -> unit Proofview.tactic
val implify : Id.t -> tactic