diff options
| author | Gaëtan Gilbert | 2019-10-05 12:16:34 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-10-05 12:16:34 +0200 |
| commit | 8398ec48072b0bbe5e571a8d1f1f6c1ace9270f4 (patch) | |
| tree | d13a1039ce27bb947e80eb63781bb64a6037dcef /doc/plugin_tutorial/Makefile | |
| parent | d7f11221f797e501fe3bcdb06fe7ef3f559869c3 (diff) | |
Remove "is_polymorphic_univ" checks in upper layers.
There were 2:
- when declaring a constraint to avoid monomorphic constraint
referring to polymorphic univs, this check is redundant with the
check in Section.ml
- when declaring a universe context to avoid redeclaring universes,
this is not necessary after recent commits.
Diffstat (limited to 'doc/plugin_tutorial/Makefile')
0 files changed, 0 insertions, 0 deletions