diff options
| author | Maxime Dénès | 2018-09-13 18:07:55 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-09-13 18:07:55 +0200 |
| commit | 8500216ac8df90b2afc0f5fd42d714cc87c6bde6 (patch) | |
| tree | 76a1ebe10646d2432f1539fb7ee9c6b0691ea221 /kernel/declarations.ml | |
| parent | 9281bb33f2b9aa5d762f8b5b8b0159984b696efb (diff) | |
| parent | 8fafc201699e3d6c80e39bbadf2e6a5ba6425036 (diff) | |
Merge PR #8436: Move maps & sets indexed by GlobRef.t into the kernel
Diffstat (limited to 'kernel/declarations.ml')
0 files changed, 0 insertions, 0 deletions