diff options
| author | Hugo Herbelin | 2015-03-25 09:44:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2015-03-25 12:11:50 +0100 |
| commit | 1a519fc37e703b014e3bcc77de01edd82aabea5f (patch) | |
| tree | 80d95a041c995c3d01e5609c39aa985f857c3b60 /kernel/declarations.mli | |
| parent | 12a77d49db68f88fc5886d6527217a761045865b (diff) | |
Another example about the consequence of a wrong computation of the
number of recursively uniform parameters in the presence of let-ins.
In practice, more recursively non-uniform parameters were assumed and
this was used especially for checking positivity of nested types,
leading to refusing more nested types than necessary (see Inductive.v).
Diffstat (limited to 'kernel/declarations.mli')
0 files changed, 0 insertions, 0 deletions