diff options
| author | Gaëtan Gilbert | 2020-02-13 16:52:33 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-19 14:09:01 +0100 |
| commit | 2ed097cfba9136a0fba9b961d24c408077fac11d (patch) | |
| tree | 6d3926e3d8aa20fd21929ad538f626660874b239 /kernel/type_errors.ml | |
| parent | 43c3c7d6f62a9bee4772242c27fbafd54770d271 (diff) | |
ComInductive: use lbound=Prop iff non polymorphic
This avoids having to interp params and intern arities twice.
Diffstat (limited to 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions