aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-03-27 20:04:24 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-03-27 20:11:31 +0100
commitd976efa0b6cfd4be2aa1d9bf8da5a4b266873b15 (patch)
tree67536d6ed621a336e6338f4e00af80bb88b2b274 /tactics/tacticals.mli
parent37f0149647336f63729b87deb17e3cd7b45c93ca (diff)
Removing tactic compatibility layer from Eqdecide.
Diffstat (limited to 'tactics/tacticals.mli')
-rw-r--r--tactics/tacticals.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index a08468865..8047281e8 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -195,7 +195,7 @@ module New : sig
THIS MODULE. *)
val tclFAIL : int -> Pp.std_ppcmds -> 'a tactic
- val tclZEROMSG : Pp.std_ppcmds -> unit tactic
+ val tclZEROMSG : Pp.std_ppcmds -> 'a tactic
(** Fail with a [User_Error] containing the given message. *)
val tclOR : unit tactic -> unit tactic -> unit tactic