aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.mli
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tactics.mli')
-rw-r--r--tactics/tactics.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c5dfeed9c..556a5a351 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -170,7 +170,7 @@ val apply_clear_request : clear_flag -> bool -> constr -> unit Proofview.tactic
val specialize : constr with_bindings -> tactic
-val move_hyp : bool -> Id.t -> Id.t move_location -> tactic
+val move_hyp : Id.t -> Id.t move_location -> tactic
val rename_hyp : (Id.t * Id.t) list -> unit Proofview.tactic
val revert : Id.t list -> unit Proofview.tactic