diff options
| author | Pierre-Marie Pédrot | 2019-10-25 11:46:59 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-10-29 13:48:57 +0100 |
| commit | 6da3091bdb249af11302042e7958f87b2cd36e63 (patch) | |
| tree | 65b516f02f4eb4b9331283e3138d6bcfd1c5ddfc /dev | |
| parent | 5651d47395c1a88b8d5a1549f14c99f81bbcb551 (diff) | |
Document the ability to bind notation arguments in Ltac2.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions