aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.mli
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-10 00:10:53 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-02-10 00:18:27 +0100
commit15fa9b62cd46a4aeeb33930d6c1272c7288b25fc (patch)
treed27afabbfb2c63af5ef54242e73d2d48e4eabbb8 /tactics/tacticals.mli
parentd3a15be9e97bf5f509b64f48d787e808866d922f (diff)
More expressive API for tclWITHHOLES.
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 03ea89ad5..4e860892d 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -218,7 +218,7 @@ module New : sig
val tclCOMPLETE : 'a tactic -> 'a tactic
val tclSOLVE : unit tactic list -> unit tactic
val tclPROGRESS : unit tactic -> unit tactic
- val tclWITHHOLES : bool -> ('a -> unit tactic) -> Evd.evar_map -> 'a -> unit tactic
+ val tclWITHHOLES : bool -> 'a tactic -> Evd.evar_map -> 'a tactic
val tclTIMEOUT : int -> unit tactic -> unit tactic
val tclTIME : string option -> 'a tactic -> 'a tactic