diff options
| author | Pierre-Marie Pédrot | 2020-11-21 15:15:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-11-30 18:46:50 +0100 |
| commit | bb97b0fef935bbd80daf944c4093a56a808fdb94 (patch) | |
| tree | 2c2f420e3885673e716acc2171c78611d76a7229 /user-contrib/Ltac2/tac2env.mli | |
| parent | b2d3d5f5d5f3e16e271a124f9f60a09788e93838 (diff) | |
Add an abstraction function in the LtacX FFI.
This allows to embed Ltac2 functions manipulating Ltac1 values as simple
Ltac1 values.
Diffstat (limited to 'user-contrib/Ltac2/tac2env.mli')
| -rw-r--r-- | user-contrib/Ltac2/tac2env.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/tac2env.mli b/user-contrib/Ltac2/tac2env.mli index af1197c24c..95dcdd7e1b 100644 --- a/user-contrib/Ltac2/tac2env.mli +++ b/user-contrib/Ltac2/tac2env.mli @@ -144,6 +144,10 @@ val ltac1_prefix : ModPath.t val wit_ltac2 : (Id.t CAst.t list * raw_tacexpr, Id.t list * glb_tacexpr, Util.Empty.t) genarg_type (** Ltac2 quotations in Ltac1 code *) +val wit_ltac2_val : (Util.Empty.t, unit, Util.Empty.t) genarg_type +(** Embedding Ltac2 closures of type [Ltac1.t -> Ltac1.t] inside Ltac1. There is + no relevant data because arguments are passed by conventional names. *) + val wit_ltac2_constr : (raw_tacexpr, Id.Set.t * glb_tacexpr, Util.Empty.t) genarg_type (** Ltac2 quotations in Gallina terms *) |