Make All universe polymorphic

Without this, TypingWf has universe inconsistencies with Gallina quotation.

Author: JasonGross

utils/theories/All_Forall.v

@@ -8,7 +8,7 @@ Derive Signature for Forall Forall2.
 (** Combinators *)
 
 (** Forall combinators in Type to allow building them by recursion *)
-Inductive All {A} (P : A -> Type) : list A -> Type :=
+Polymorphic Cumulative Inductive All {A} (P : A -> Type) : list A -> Type :=
     All_nil : All P []
   | All_cons : forall (x : A) (l : list A),
                   P x -> All P l -> All P (x :: l).
@@ -3563,6 +3563,7 @@ Proof.
   all: now apply In_All; constructor => //.
 Qed.
 
+Local Set Universe Polymorphism.
 Lemma All_eta3 {A B C P} ls
   : @All (A * B * C)%type (fun '(a, b, c) => P a b c) ls <~> All (fun abc => P abc.1.1 abc.1.2 abc.2) ls.
 Proof.