diff options
Diffstat (limited to 'engine/proofview.mli')
| -rw-r--r-- | engine/proofview.mli | 17 |
1 files changed, 13 insertions, 4 deletions
diff --git a/engine/proofview.mli b/engine/proofview.mli index 286703c0dc..680a93f0cc 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -156,10 +156,15 @@ type +'a tactic tactic has given up. In case of multiple success the first one is selected. If there is no success, fails with {!Logic_monad.TacticFailure}*) -val apply : Environ.env -> 'a tactic -> proofview -> 'a - * proofview - * (bool*Evar.t list*Evar.t list) - * Proofview_monad.Info.tree +val apply + : name:Names.Id.t + -> poly:bool + -> Environ.env + -> 'a tactic + -> proofview + -> 'a * proofview + * (bool*Evar.t list*Evar.t list) + * Proofview_monad.Info.tree (** {7 Monadic primitives} *) @@ -407,6 +412,10 @@ val tclTIMEOUT : int -> 'a tactic -> 'a tactic identifying annotation if present *) val tclTIME : string option -> 'a tactic -> 'a tactic +(** Internal, don't use. *) +val tclProofInfo : (Names.Id.t * bool) tactic +[@@ocaml.deprecated "internal, don't use"] + (** {7 Unsafe primitives} *) (** The primitives in the [Unsafe] module should be avoided as much as |