diff options
| author | Pierre-Marie Pédrot | 2020-02-15 11:56:40 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-03-18 18:24:44 +0100 |
| commit | 70bc1e9c5122ad5a8a3dc78aae764afc65b4dead (patch) | |
| tree | 68396484f0a62cdf55dc8e0723d67743c102e68f /user-contrib/Ltac2/tac2ffi.mli | |
| parent | 9d533d1b851b9504599778a77dd32724d6b39219 (diff) | |
Actually use the binder type for Ltac2 that should be used in the kernel.
That is, it contains the type of the binder so as not to rely on the relevance
explicitly.
Diffstat (limited to 'user-contrib/Ltac2/tac2ffi.mli')
| -rw-r--r-- | user-contrib/Ltac2/tac2ffi.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli index 5138133360..c9aa50389e 100644 --- a/user-contrib/Ltac2/tac2ffi.mli +++ b/user-contrib/Ltac2/tac2ffi.mli @@ -180,7 +180,7 @@ val val_constant : Constant.t Val.tag val val_constructor : constructor Val.tag val val_projection : Projection.t Val.tag val val_case : Constr.case_info Val.tag -val val_binder : Name.t Context.binder_annot Val.tag +val val_binder : (Name.t Context.binder_annot * types) Val.tag val val_univ : Univ.Level.t Val.tag val val_free : Id.Set.t Val.tag val val_ltac1 : Geninterp.Val.t Val.tag |