From 3862664c87046abc2808eddbaa6b1a2033e9454e Mon Sep 17 00:00:00 2001
From: Dan Christensen <jdc@uwo.ca>
Date: Wed, 6 Nov 2024 20:24:02 -0500
Subject: [PATCH] Matrix: use strip_reflections to avoid extra universe
 variables

---
 theories/Algebra/Rings/Matrix.v | 14 ++++++++------
 1 file changed, 8 insertions(+), 6 deletions(-)

diff --git a/theories/Algebra/Rings/Matrix.v b/theories/Algebra/Rings/Matrix.v
index d1fe1d13c3..4b9e1d2499 100644
--- a/theories/Algebra/Rings/Matrix.v
+++ b/theories/Algebra/Rings/Matrix.v
@@ -5,6 +5,7 @@ Require Import Algebra.Rings.Ring Algebra.Rings.Module Algebra.Rings.CRing
   Algebra.Rings.KroneckerDelta Algebra.Rings.Vector.
 Require Import abstract_algebra.
 Require Import WildCat.Core WildCat.Paths.
+Require Import Modalities.ReflectiveSubuniverse.
 
 Set Universe Minimization ToSet.
 
@@ -692,12 +693,13 @@ Proof.
 Defined.
 
 (** The sum of two upper triangular matrices is upper triangular. *)
-Global Instance upper_triangular_plus {R : Ring@{i}} {n : nat} (M N : Matrix R n n)
+Global Instance upper_triangular_plus@{i} {R : Ring@{i}} {n : nat} (M N : Matrix R n n)
   {H1 : IsUpperTriangular M} {H2 : IsUpperTriangular N}
   : IsUpperTriangular (matrix_plus M N).
 Proof.
   unfold IsUpperTriangular.
-  strip_truncations; apply tr.
+  (* We use [strip_reflections] rather than [strip_truncations] here and below because it generates fewer universe variables in some versions of Coq. *)
+  strip_reflections; apply tr.
   intros i j Hi Hj lt_i_j.
   specialize (H1 i j Hi Hj lt_i_j).
   specialize (H2 i j Hi Hj lt_i_j).
@@ -718,12 +720,12 @@ Proof.
 Defined.
 
 (** The negation of an upper triangular matrix is upper triangular. *)
-Global Instance upper_triangular_negate {R : Ring@{i}} {n : nat} (M : Matrix R n n)
+Global Instance upper_triangular_negate@{i} {R : Ring@{i}} {n : nat} (M : Matrix R n n)
   {H : IsUpperTriangular M}
   : IsUpperTriangular (matrix_negate M).
 Proof.
   unfold IsUpperTriangular.
-  strip_truncations; apply tr.
+  strip_reflections; apply tr.
   intros i j Hi Hj lt_i_j.
   rewrite entry_Build_Matrix.
   rewrite <- rng_negate_zero; f_ap.
@@ -741,12 +743,12 @@ Proof.
 Defined.
 
 (** The product of two upper triangular matrices is upper triangular. *)
-Global Instance upper_triangular_mult {R : Ring@{i}} {n : nat}
+Global Instance upper_triangular_mult@{i} {R : Ring@{i}} {n : nat}
   (M N : Matrix R n n) {H1 : IsUpperTriangular M} {H2 : IsUpperTriangular N}
   : IsUpperTriangular (matrix_mult M N).
 Proof.
   unfold IsUpperTriangular.
-  strip_truncations; apply tr.
+  strip_reflections; apply tr.
   intros i j Hi Hj lt_i_j.
   rewrite entry_Build_Matrix.
   apply ab_sum_zero.