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).

0 files changed, 0 insertions, 0 deletions