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 /dev/include | |
| 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 'dev/include')
0 files changed, 0 insertions, 0 deletions