diff options
| author | Pierre-Marie Pédrot | 2017-07-28 17:53:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-07-30 00:20:30 +0200 |
| commit | 0f72b089de52ad7d26d71e56003b140fa5012635 (patch) | |
| tree | 9fe0d82fc1c30e0a4740dfc23a876e0a8aa817a9 /theories/Control.v | |
| parent | 23f10f3a1a0fd6498cad975b39af5dd3a8559f06 (diff) | |
Exporting more internals from Coq implementation.
Diffstat (limited to 'theories/Control.v')
| -rw-r--r-- | theories/Control.v | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/theories/Control.v b/theories/Control.v index a6d46a89a8..a8b92aced2 100644 --- a/theories/Control.v +++ b/theories/Control.v @@ -54,3 +54,10 @@ Ltac2 @ external hyps : unit -> (ident * constr option * constr) list := "ltac2" (** Refinement *) Ltac2 @ external refine : (unit -> constr) -> unit := "ltac2" "refine". + +(** Evars *) + +Ltac2 @ external with_holes : (unit -> 'a) -> ('a -> 'b) -> 'b := "ltac2" "with_holes". +(** [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. *) |