diff options
| author | Pierre-Marie Pédrot | 2019-10-02 09:31:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-29 13:48:57 +0100 |
| commit | 5651d47395c1a88b8d5a1549f14c99f81bbcb551 (patch) | |
| tree | 8f674737cb1dce8b91f1f8930047ee155c994baf /user-contrib/Ltac2/tac2ffi.mli | |
| parent | 5370e79c1128dd96a75e3c37569daa3fd98dcd86 (diff) | |
Fix #10615: Notation substitution for Ltac2 terms.
We implement a new type of "preterms" that represent untyped ASTs, corresponding
to glob_expr in the ML implementations. Ltac2 quotations inside notations are
provided with such preterms, and have to pretype them in order to do anything
of relevance with them.
Diffstat (limited to 'user-contrib/Ltac2/tac2ffi.mli')
| -rw-r--r-- | user-contrib/Ltac2/tac2ffi.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/user-contrib/Ltac2/tac2ffi.mli b/user-contrib/Ltac2/tac2ffi.mli index 480eee51fc..d3c9596e8f 100644 --- a/user-contrib/Ltac2/tac2ffi.mli +++ b/user-contrib/Ltac2/tac2ffi.mli @@ -165,6 +165,7 @@ val valexpr : valexpr repr val val_constr : EConstr.t Val.tag val val_ident : Id.t Val.tag val val_pattern : Pattern.constr_pattern Val.tag +val val_preterm : Ltac_pretype.closed_glob_constr Val.tag val val_pp : Pp.t Val.tag val val_sort : ESorts.t Val.tag val val_cast : Constr.cast_kind Val.tag |