diff options
| author | Pierre-Marie Pédrot | 2016-05-03 15:06:11 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-05-03 16:05:08 +0200 |
| commit | b6e796a8ef956fa25bfeba84545f25b2cfb3aaf9 (patch) | |
| tree | da87235dd73f6425ea980100894ccc910a0ec877 /kernel/nativelambda.mli | |
| parent | 00a13c3c014e2729d17ad8e8191f20586ae3b52b (diff) | |
Fix bug #3825: Universe annotations on notations should pass through or be rejected.
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions