diff options
| author | Enrico Tassi | 2019-01-29 11:23:44 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2019-01-29 11:23:44 +0100 |
| commit | a9b141469fe3036355be95d8cf5f0bf5c240fe37 (patch) | |
| tree | 1ced7154c46778ec3135bc024e6a640ae205ca6e /kernel/context.ml | |
| parent | 1f3536e89b7235aaa0007e8ab7298040407df8ba (diff) | |
| parent | da420fd8315db308a013bb3cca3512fd9c9bf627 (diff) | |
Merge PR #9421: [vernac] Fix classification of `Declare Custom Entry`
Reviewed-by: gares
Diffstat (limited to 'kernel/context.ml')
0 files changed, 0 insertions, 0 deletions