From f820715a7a5f6ff120dc85f870d4a328ab30c160 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 1 Apr 2023 22:14:03 -0700
Subject: [PATCH 1/2] Make All universe polymorphic

Without this, TypingWf has universe inconsistencies with Gallina quotation.
---
 utils/theories/All_Forall.v | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/utils/theories/All_Forall.v b/utils/theories/All_Forall.v
index fdf7e56ce..22c318abc 100644
--- a/utils/theories/All_Forall.v
+++ b/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.

From 8afa771190737f28faba6cfc0dda937e18c2fb31 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Sat, 1 Apr 2023 22:44:12 -0700
Subject: [PATCH 2/2] Make all of All_Forall universe polymorphic

Turns out All isn't enough.
---
 utils/theories/All_Forall.v | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/utils/theories/All_Forall.v b/utils/theories/All_Forall.v
index 22c318abc..52cd1adbf 100644
--- a/utils/theories/All_Forall.v
+++ b/utils/theories/All_Forall.v
@@ -3,12 +3,16 @@ From MetaCoq.Utils Require Import MCPrelude MCReflect MCList MCRelations MCProd
 From Equations Require Import Equations.
 Import ListNotations.
 
+Local Set Universe Polymorphism.
+Local Set Polymorphic Inductive Cumulativity.
+Local Unset Universe Minimization ToSet.
+
 Derive Signature for Forall Forall2.
 
 (** Combinators *)
 
 (** Forall combinators in Type to allow building them by recursion *)
-Polymorphic Cumulative Inductive All {A} (P : A -> Type) : list A -> Type :=
+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,7 +3567,6 @@ 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.