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.

1 files changed, 24 insertions, 20 deletions

diff --git a/test-suite/bugs/closed/3446.v b/test-suite/bugs/closed/3446.v
index 4f29b76c6..dce73e1a5 100644
--- a/test-suite/bugs/closed/3446.v
+++ b/test-suite/bugs/closed/3446.v
@@ -1,28 +1,32 @@
 (* File reduced by coq-bug-finder from original input, then from 7372 lines to 539 lines, then from 531 lines to 107 lines, then from 76 lines to 46 lines *)
-(* Set Asymmetric Patterns. *)
-(* Reserved Notation "x -> y" (at level 99, right associativity, y at level 200). *)
-(* Notation "A -> B" := (forall (_ : A), B). *)
+Module First.
+Set Asymmetric Patterns.
+Reserved Notation "x -> y" (at level 99, right associativity, y at level 200).
+Notation "A -> B" := (forall (_ : A), B).
+Set Universe Polymorphism.
+
 
-(* Notation "x → y" := (x -> y) *)
-(*   (at level 99, y at level 200, right associativity): type_scope. *)
-(* Record sigT A (P : A -> Type) := *)
-(*   { projT1 : A ; projT2 : P projT1 }. *)
-(* Arguments projT1 {A P} s. *)
-(* Arguments projT2 {A P} s. *)
-(* Set Universe Polymorphism. *)
-(* Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x). *)
-(* Reserved Notation "x = y" (at level 70, no associativity). *)
-(* Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y). *)
-(* Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end. *)
-(* Reserved Notation "{ x : A  & P }" (at level 0, x at level 99). *)
-(* Notation "{ x : A  & P }" := (sigT A (fun x => P)) : type_scope. *)
+Notation "x → y" := (x -> y)
+  (at level 99, y at level 200, right associativity): type_scope.
+Record sigT A (P : A -> Type) :=
+  { projT1 : A ; projT2 : P projT1 }.
+Arguments projT1 {A P} s.
+Arguments projT2 {A P} s.
+Definition compose {A B C : Type} (g : B -> C) (f : A -> B) := fun x => g (f x).
+Reserved Notation "x = y" (at level 70, no associativity).
+Inductive paths {A : Type} (a : A) : A -> Type := idpath : paths a a where "x = y" := (@paths _ x y).
+Notation " x = y " := (paths x y) : type_scope.
+Definition transport {A : Type} (P : A -> Type) {x y : A} (p : x = y) (u : P x) : P y := match p with idpath => u end.
+Reserved Notation "{ x : A  & P }" (at level 0, x at level 99).
+Notation "{ x : A  & P }" := (sigT A (fun x => P)) : type_scope.
 
 
-(* Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v &  transport _ p (projT2 u) = projT2 v}), u = v. *)
-(* Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}). *)
+Axiom path_sigma_uncurried : forall {A : Type} (P : A -> Type) (u v : sigT A P) (pq : {p : projT1 u = projT1 v &  transport _ p (projT2 u) = projT2 v}), u = v.
+Axiom isequiv_pr1_contr : forall {A} {P : A -> Type}, (A -> {x : A & P x}).
 
-(* Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) := *)
-(*   @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _). *)
+Definition path_sigma_hprop {A : Type} {P : A -> Type} (u v : sigT _ P) :=
+  @compose _ _ _ (path_sigma_uncurried P u v) (@isequiv_pr1_contr _ _).
+End First.
 
 Set Asymmetric Patterns.
 Set Universe Polymorphism.