diff options
| author | Andres Erbsen | 2020-02-12 16:22:06 -0500 |
|---|---|---|
| committer | Andres Erbsen | 2020-02-14 15:08:11 -0500 |
| commit | 09252f6b060321985f2d82aa130ac7e3d6147025 (patch) | |
| tree | bbad8009bd50bb14f4735f2dc8bf5d8fb92bb7a8 /dev/tools/pre-commit | |
| parent | 097f779646fe8fedfeff99e2716b11e36e0aa80a (diff) | |
test for x[i] notation not breaking Ltac parsing
Diffstat (limited to 'dev/tools/pre-commit')
0 files changed, 0 insertions, 0 deletions