Fix bug #4254 with the help of J.H. Jourdan

1) We now _assign_ the smallest possible arities to mutual inductive types
and eventually add leq constraints on the user given arities. Remove
useless limitation on instantiating algebraic universe variables with
their least upper bound if they have upper constraints as well.

2) Do not remove non-recursive variables when computing minimal levels of inductives.

3) Avoid modifying user-given arities if not necessary to compute the
minimal level of an inductive.

4) We correctly solve the recursive equations taking into account the
user-declared level.

0 files changed, 0 insertions, 0 deletions