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 /doc/plugin_tutorial/tuto2/src/custom.ml | |
| 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 'doc/plugin_tutorial/tuto2/src/custom.ml')
0 files changed, 0 insertions, 0 deletions