diff options
Diffstat (limited to 'user-contrib/Ltac2/Ltac1.v')
| -rw-r--r-- | user-contrib/Ltac2/Ltac1.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/Ltac1.v b/user-contrib/Ltac2/Ltac1.v index 1a69708a7d..fd1555c2fb 100644 --- a/user-contrib/Ltac2/Ltac1.v +++ b/user-contrib/Ltac2/Ltac1.v @@ -25,6 +25,12 @@ Ltac2 @ external run : t -> unit := "ltac2" "ltac1_run". (** Runs an Ltac1 value, assuming it is a 'tactic', i.e. not returning anything. *) +Ltac2 @ external lambda : (t -> t) -> t := "ltac2" "ltac1_lambda". +(** Embed an Ltac2 function into Ltac1 values. Contrarily to the ltac1:(...) + quotation, this function allows both to capture an Ltac2 context inside the + closure and to return an Ltac1 value. Returning values in Ltac1 is a + intrepid endeavour prone to weird runtime semantics. *) + Ltac2 @ external apply : t -> t list -> (t -> unit) -> unit := "ltac2" "ltac1_apply". (** Applies an Ltac1 value to a list of arguments, and provides the result in CPS style. It does **not** run the returned value. *) |