diff options
| author | Gaëtan Gilbert | 2017-09-21 11:14:11 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-11-25 14:18:35 +0100 |
| commit | d071eac98b7812ac5c03004b438022900885d874 (patch) | |
| tree | f0f72dba7daf7c91ea2eda0332b568c4615ad3c9 /API/API.mli | |
| parent | 765392492df2f5e065b2b5e706b6620846337cc0 (diff) | |
Forbid repeated names in universe binders.
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions