aboutsummaryrefslogtreecommitdiff
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 81f63fc22b..411cc38f43 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -160,7 +160,7 @@ val clear : Id.t list -> tactic
val clear_body : Id.t list -> tactic
val keep : Id.t list -> tactic
-val specialize : int option -> constr with_bindings -> tactic
+val specialize : constr with_bindings -> tactic
val move_hyp : bool -> Id.t -> Id.t move_location -> tactic
val rename_hyp : (Id.t * Id.t) list -> tactic