diff options
Diffstat (limited to 'theories/Control.v')
| -rw-r--r-- | theories/Control.v | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/theories/Control.v b/theories/Control.v index a8b92aced2..071c2ea8ce 100644 --- a/theories/Control.v +++ b/theories/Control.v @@ -34,6 +34,8 @@ Ltac2 @ external new_goal : evar -> unit := "ltac2" "new_goal". already defined in the current state, don't do anything. Panics if the evar is not in the current state. *) +Ltac2 @ external progress : (unit -> 'a) -> 'a := "ltac2" "progress". + (** Goal inspection *) Ltac2 @ external goal : unit -> constr := "ltac2" "goal". @@ -61,3 +63,14 @@ Ltac2 @ external with_holes : (unit -> 'a) -> ('a -> 'b) -> 'b := "ltac2" "with_ (** [with_holes x f] evaluates [x], then apply [f] to the result, and fails if all evars generated by the call to [x] have not been solved when [f] returns. *) + +(** Misc *) + +Ltac2 @ external time : string option -> (unit -> 'a) -> 'a := "ltac2" "time". +(** Displays the time taken by a tactic to evaluate. *) + +Ltac2 @ external abstract : ident option -> (unit -> unit) -> unit := "ltac2" "abstract". +(** Abstract a subgoal. *) + +Ltac2 @ external check_interrupt : unit -> unit := "ltac2" "check_interrupt". +(** For internal use. *) |