From 11b82b14d98573e72c6f14ee4c110e21920b9ceb Mon Sep 17 00:00:00 2001
From: Pierre Casteran <pierre.casteran@labri.fr>
Date: Fri, 26 Jan 2024 11:36:04 +0100
Subject: [PATCH 1/2] minor change

---
 theories/ordinals/Epsilon0/Canon.v | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/theories/ordinals/Epsilon0/Canon.v b/theories/ordinals/Epsilon0/Canon.v
index 67f933d0..68cbb8ae 100644
--- a/theories/ordinals/Epsilon0/Canon.v
+++ b/theories/ordinals/Epsilon0/Canon.v
@@ -1046,9 +1046,9 @@ Lemma CanonSSn (i:nat) :
                     CanonS (Cons alpha (S n) E0zero) i =
                     Cons alpha n (CanonS (E0_phi0 alpha) i).
 Proof.
-  intros; apply E0_eq_intro;
-  unfold CanonS;repeat (rewrite cnf_rw || rewrite cnf_Cons); auto.
-  - unfold canonS; rewrite canon_SSn_zero; auto with E0.
+  intros; apply E0_eq_intro.
+  unfold Canon;  repeat (rewrite cnf_rw || rewrite cnf_Cons); auto.
+  -  rewrite canon_SSn_zero; auto with E0.
   -  unfold lt, E0_phi0; repeat rewrite cnf_rw. 
      apply canonS_LT ; trivial. 
      apply nf_phi0;auto with E0. 

From 7613b5015389eee356214f5593b1aa9b40d014bf Mon Sep 17 00:00:00 2001
From: Pierre Casteran <pierre.casteran@labri.fr>
Date: Sun, 28 Jan 2024 11:44:01 +0100
Subject: [PATCH 2/2] Data type associated with an ordinal notation is now a
 coercio

---
 theories/ordinals/Hydra/Omega2_Small.v          | 2 +-
 theories/ordinals/OrdinalNotations/ON_Generic.v | 4 ++++
 theories/ordinals/OrdinalNotations/ON_Omega2.v  | 1 -
 3 files changed, 5 insertions(+), 2 deletions(-)

diff --git a/theories/ordinals/Hydra/Omega2_Small.v b/theories/ordinals/Hydra/Omega2_Small.v
index 95eac6c8..c06b32b4 100644
--- a/theories/ordinals/Hydra/Omega2_Small.v
+++ b/theories/ordinals/Hydra/Omega2_Small.v
@@ -19,7 +19,7 @@ Section Impossibility_Proof.
   
   (* begin snippet Impossibilitya *)
   
-  Variable m : Hydra -> ON_Omega2.t.
+  Variable m : Hydra -> rep Omega2.
   Context
     (Hvar: Hvariant Omega2 free m).
 
diff --git a/theories/ordinals/OrdinalNotations/ON_Generic.v b/theories/ordinals/OrdinalNotations/ON_Generic.v
index 47ef853a..fa260056 100644
--- a/theories/ordinals/OrdinalNotations/ON_Generic.v
+++ b/theories/ordinals/OrdinalNotations/ON_Generic.v
@@ -30,6 +30,10 @@ Class ON {A:Type} (lt: relation A) (cmp: Compare A) :=
 #[global] Existing Instance ON_comp.
 Coercion ON_wf :  ON >-> well_founded.
 
+Definition rep {A:Type} {lt: relation A} {cmp: Compare A}
+                (on : ON lt cmp) := A. 
+
+#[global] Coercion rep : ON >-> Sortclass.
 (* end snippet ONDef *)
 
 (* begin snippet ONDefsa:: no-out  *)
diff --git a/theories/ordinals/OrdinalNotations/ON_Omega2.v b/theories/ordinals/OrdinalNotations/ON_Omega2.v
index f85a6b6a..35b7ce2c 100644
--- a/theories/ordinals/OrdinalNotations/ON_Omega2.v
+++ b/theories/ordinals/OrdinalNotations/ON_Omega2.v
@@ -498,7 +498,6 @@ Proof.
  - abstract lia.
 Qed.
 
-
 Lemma ap_cases alpha : ap alpha -> alpha = 1 \/ alpha = omega.
 Proof.
   destruct (zero_limit_succ_dec alpha) as [[Hzero |  Hlim] | Hsucc].