aboutsummaryrefslogtreecommitdiff
path: root/tactics/equality.mli
diff options
context:
space:
mode:
authoraspiwack2013-11-02 15:35:13 +0000
committeraspiwack2013-11-02 15:35:13 +0000
commit1f226a80efeeb65afaaa4fb203a68eac98c7619f (patch)
tree1222697edd56b72c0c7a32c43f333ae6c573ed97 /tactics/equality.mli
parent80f2f9462205193885f054338ab28bfcd17de965 (diff)
Clean up a warning.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16978 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/equality.mli')
-rw-r--r--tactics/equality.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 3bb204cafa..24c9095813 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -128,7 +128,7 @@ type subst_tactic_flags = {
}
val subst_gen : bool -> Id.t list -> unit Proofview.tactic
val subst : Id.t list -> unit Proofview.tactic
-val subst_all : ?flags:subst_tactic_flags -> unit Proofview.tactic
+val subst_all : ?flags:subst_tactic_flags -> unit -> unit Proofview.tactic
(* Replace term *)
(* [replace_multi_term dir_opt c cl]