diff options
| author | Vincent Laporte | 2018-09-26 13:39:36 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2018-09-26 13:39:36 +0000 |
| commit | 8c3f395e52020f82822100730026a950c3653c8c (patch) | |
| tree | 1d5d6997eb9ace3857d12fabaaa21a3de3250102 /kernel/type_errors.ml | |
| parent | 3f486b2334fa3a5ab7774e212a5c592ba241535c (diff) | |
| parent | 697bfeba6f5bdff48b254092a3f7f6616080e9b2 (diff) | |
Merge PR #8504: Allow successive attributes #[foo] #[bar]
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions