diff options
| author | Emilio Jesus Gallego Arias | 2018-07-30 00:03:37 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-07-30 00:03:37 +0200 |
| commit | dd84c113a154742dff86328ebc758097e9aac8eb (patch) | |
| tree | 67795fb720516f564d074d55d9e2aa90e3d4e7f2 /kernel/declarations.ml | |
| parent | 231f679965745a4d7677166e8d5f62a38ebde4e7 (diff) | |
| parent | 569ad299a8092778611fcc8ae2842151c4b276db (diff) | |
Merge PR #8115: Support for custom entries in notations (take 2, feature part)
Diffstat (limited to 'kernel/declarations.ml')
0 files changed, 0 insertions, 0 deletions