diff options
| author | Gaëtan Gilbert | 2019-09-27 17:26:26 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-02 14:38:48 +0200 |
| commit | 994edaf989c0232b5c7de70a2f8ccb46c557da95 (patch) | |
| tree | 46f5633c8e3e351a232836f951b8946f71dcf256 /dev/base_include | |
| parent | 77fd11a9f012a2878e13451e9d8a9f500c6392eb (diff) | |
Loosen restrictions on mixing universe mono/polymorphism in sections
We disallow adding univ constraints wich refer to polymorphic
universes, and monomorphic constants and inductives when polymorphic
universes or constraints are present.
Every other combination is already correctly discharged by the kernel.
Diffstat (limited to 'dev/base_include')
0 files changed, 0 insertions, 0 deletions