From 6523c89ba6ab68f77bf36bf29b9afe252c058fa3 Mon Sep 17 00:00:00 2001
From: Ali Caglayan <alizter@gmail.com>
Date: Mon, 18 Sep 2023 15:39:58 +0100
Subject: [PATCH] chore: fix 8.18 warnings

Signed-off-by: Ali Caglayan <alizter@gmail.com>
---
 theories/Basics/Equivalences.v                 |  3 ++-
 theories/Categories/LaxComma/Core.v            |  4 ++--
 .../Classes/implementations/peano_naturals.v   | 18 ++++++++++++------
 theories/Colimits/Pushout.v                    |  6 ++++--
 4 files changed, 20 insertions(+), 11 deletions(-)

diff --git a/theories/Basics/Equivalences.v b/theories/Basics/Equivalences.v
index a9a0c5833a8..dd7d883b5b1 100644
--- a/theories/Basics/Equivalences.v
+++ b/theories/Basics/Equivalences.v
@@ -93,6 +93,7 @@ Section IsEquivHomotopic.
   Let sect := (fun a:A => (ap f^-1 (h a))^ @ eissect f a).
 
   (* We prove the triangle identity with rewrite tactics.  Since we lose control over the proof term that way, we make the result opaque with "Qed". *)
+  #[clearbody]
   Let adj (a : A) : retr (g a) = ap g (sect a).
   Proof.
     unfold sect, retr.
@@ -101,7 +102,7 @@ Section IsEquivHomotopic.
     rewrite ap_V; apply moveL_Vp.
     rewrite <- ap_compose; rewrite (concat_A1p (eisretr f) (h a)).
     apply whiskerR, eisadj.
-  Qed.
+  Defined.
 
   (* This should not be an instance; it can cause the unifier to spin forever searching for functions to be homotopic to. *)
   Definition isequiv_homotopic : IsEquiv g
diff --git a/theories/Categories/LaxComma/Core.v b/theories/Categories/LaxComma/Core.v
index 212d8746ce1..3525c8f1fab 100644
--- a/theories/Categories/LaxComma/Core.v
+++ b/theories/Categories/LaxComma/Core.v
@@ -175,7 +175,7 @@ Module Export LaxCommaCoreNotations.
   (** We play some games to get nice notations for lax comma categories. *)
   Section tc_notation_boiler_plate.
     Local Open Scope type_scope.
-    Class LCC_Builder {A B C} (x : A) (y : B) (z : C) := lcc_builder_dummy : True.
+    Class LCC_Builder {A B C} (x : A) (y : B) (z : C) : Type0 := lcc_builder_dummy : True.
     Definition get_LCC `{@LCC_Builder A B C x y z} : C := z.
 
     Global Arguments get_LCC / {A B C} x y {z} {_}.
@@ -210,7 +210,7 @@ Module Export LaxCommaCoreNotations.
     : LCC_Builder (@sub_pre_cat _ P HF) a (@lax_coslice_category_over _ P HF a _) | 10
       := I.
 
-    Class OLCC_Builder {A B C} (x : A) (y : B) (z : C) := olcc_builder_dummy : True.
+    Class OLCC_Builder {A B C} (x : A) (y : B) (z : C) : Type0 := olcc_builder_dummy : True.
 
     Definition get_OLCC `{@OLCC_Builder A B C x y z} : C := z.
 
diff --git a/theories/Classes/implementations/peano_naturals.v b/theories/Classes/implementations/peano_naturals.v
index 7ac1d9bf4ab..63a5363e99a 100644
--- a/theories/Classes/implementations/peano_naturals.v
+++ b/theories/Classes/implementations/peano_naturals.v
@@ -18,8 +18,9 @@ Universe N.
 
 Let natpaths := @paths@{N} nat.
 Infix "=N=" := natpaths.
+#[clearbody]
 Let natpaths_symm : Symmetric@{N N} natpaths.
-Proof. unfold natpaths;apply _. Qed.
+Proof. unfold natpaths;apply _. Defined.
 
 Global Instance nat_0: Zero@{N} nat := 0%nat.
 Global Instance nat_1: One@{N} nat := 1%nat.
@@ -582,19 +583,23 @@ Section for_another_semiring.
 
 (*   Add Ring R: (rings.stdlib_semiring_theory R). *)
 
+  #[clearbody]
   Let f_preserves_0: toR 0 =  0.
-  Proof. reflexivity. Qed.
+  Proof. reflexivity. Defined.
 
+  #[clearbody]
   Let f_preserves_1: toR 1 = 1.
-  Proof. reflexivity. Qed.
+  Proof. reflexivity. Defined.
 
+  #[clearbody]
   Let f_S : forall x, toR (S x) = 1 + toR x.
   Proof.
   intros [|x].
   - symmetry;apply plus_0_r.
   - reflexivity.
-  Qed.
+  Defined.
 
+  #[clearbody]
   Let f_preserves_plus a a': toR (a + a') = toR a + toR a'.
   Proof.
   induction a as [|a IHa].
@@ -603,8 +608,9 @@ Section for_another_semiring.
   - change (toR (S (a + a')) = toR (S a) + toR a').
     rewrite !f_S,IHa.
     apply associativity.
-  Qed.
+  Defined.
 
+  #[clearbody]
   Let f_preserves_mult a a': toR (a * a') = toR a * toR a'.
   Proof.
   induction a as [|a IHa].
@@ -615,7 +621,7 @@ Section for_another_semiring.
     rewrite f_preserves_plus, IHa.
     rewrite plus_mult_distr_r,mult_1_l.
     reflexivity.
-  Qed.
+  Defined.
 
   Global Instance nat_to_sr_morphism
     : IsSemiRingPreserving (naturals_to_semiring nat R).
diff --git a/theories/Colimits/Pushout.v b/theories/Colimits/Pushout.v
index daf6ca19bc1..96e05e3ad5a 100644
--- a/theories/Colimits/Pushout.v
+++ b/theories/Colimits/Pushout.v
@@ -269,6 +269,7 @@ Section EquivSigmaPushout.
     + intros a; cbn. exact (pglue (x;a)).
   Defined.
 
+  #[clearbody]
   Let esp1_beta_pglue (x : X) (a : A x)
     : ap esp1 (path_sigma' (fun x => Pushout (f x) (g x)) 1 (pglue a))
       = pglue (x;a).
@@ -278,7 +279,7 @@ Section EquivSigmaPushout.
     rewrite !concat_p1.
     unfold esp1; rewrite Pushout_rec_beta_pglue.
     reflexivity.
-  Qed.
+  Defined.
 
   Let esp2 : Pushout (functor_sigma idmap f) (functor_sigma idmap g)
              -> { x : X & Pushout (f x) (g x) }.
@@ -291,13 +292,14 @@ Section EquivSigmaPushout.
       apply pglue.
   Defined.
 
+  #[clearbody]
   Let esp2_beta_pglue (x : X) (a : A x)
     : ap esp2 (pglue (x;a)) = path_sigma' (fun x:X => Pushout (f x) (g x)) 1 (pglue a).
   Proof.
     unfold esp2.
     rewrite Pushout_rec_beta_pglue.
     reflexivity.
-  Qed.
+  Defined.
 
   Definition equiv_sigma_pushout
     : { x : X & Pushout (f x) (g x) }