diff options
| author | Pierre-Marie Pédrot | 2018-11-05 11:21:01 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-05 11:21:01 +0100 |
| commit | 3517dc938efbc4f7b3c5383bdc5b7e20dc14b2f3 (patch) | |
| tree | fb37ff693237199e7ac2cb252e2dd5371a459e8d /library/libobject.ml | |
| parent | 67ab9b444995ac216e908a0963192304d4965e69 (diff) | |
| parent | bc1ea6aaa7dd18b1aa3591a4caf8152d66e02e52 (diff) | |
Merge PR #8766: [nametab] [api] Provide basic support for efficient completion.
Diffstat (limited to 'library/libobject.ml')
0 files changed, 0 insertions, 0 deletions