diff options
| author | Gaëtan Gilbert | 2019-09-24 10:23:06 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-09-24 10:23:06 +0200 |
| commit | f92b5e4a91e8edb7ccac2ebe64d68c8d89e2e0db (patch) | |
| tree | 3f72fbbe405333b16fafcad5f9e30d95fd337de4 /library/lib.mli | |
| parent | dc690e7067aa91a05472b5d573cb463223ef4dec (diff) | |
Fix #10783: use binder_annot in Ltac2.Constr.Unsafe.kind
Diffstat (limited to 'library/lib.mli')
0 files changed, 0 insertions, 0 deletions