diff options
| author | Pierre-Marie Pédrot | 2020-07-26 15:47:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-07-26 15:47:57 +0200 |
| commit | 91aef2ce0368b017bb20d7b683b907eb2a1847a9 (patch) | |
| tree | 498ea9e76bbfcf816d2c07ec4793836b8c4fbe79 /kernel/type_errors.ml | |
| parent | 55f4095fe3c366a9f310584a55e2dc0605e5409c (diff) | |
| parent | 37ba76b1ba6f4f5edcf05d69e6a21a46fef026d9 (diff) | |
Merge PR #12573: Hint Opaque/Transparent/Unfold: don't error on Opaque Defined constants
Reviewed-by: ppedrot
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions