From 14bf0def33bc66b66210696ac76dbe91b4e8811c Mon Sep 17 00:00:00 2001
From: Pierre Casteran <pierre.casteran@labri.fr>
Date: Tue, 23 Jan 2024 14:54:07 +0100
Subject: [PATCH] Add a coercion from ON to Wf

---
 theories/ordinals/Hydra/Hydra_Termination.v     |  7 +++----
 theories/ordinals/Hydra/Omega2_Small.v          |  2 +-
 theories/ordinals/Hydra/Omega_Small.v           | 10 ++++------
 theories/ordinals/OrdinalNotations/ON_Generic.v |  4 +++-
 4 files changed, 11 insertions(+), 12 deletions(-)

diff --git a/theories/ordinals/Hydra/Hydra_Termination.v b/theories/ordinals/Hydra/Hydra_Termination.v
index 403edebe..2a3735db 100644
--- a/theories/ordinals/Hydra/Hydra_Termination.v
+++ b/theories/ordinals/Hydra/Hydra_Termination.v
@@ -7,6 +7,7 @@ Set Program Cases.
 
 From hydras Require Export Hydra_Lemmas.
 From hydras Require Import E0 Hessenberg.
+Import ON_Generic. 
 
 (** ***  Converting any hydra into an ordinal less than 
   #epsilon0# $\epsilon_0$  
@@ -194,8 +195,7 @@ Qed.
 #[ global, program ] Instance var (h:Hydra) : E0:= @mkord (m h) _.
 Next Obligation. apply m_nf. Defined.
 
-
-#[global] Instance HVariant_0 : @Hvariant _ _ T1_wf free m.
+#[global] Instance HVariant_0 : Hvariant T1_wf free m.
 Proof.
  split; intros; eapply round_decr; eauto.
 Qed.
@@ -204,8 +204,7 @@ Qed.
 (* begin snippet FinalThm *)
 
 (*| .. coq:: no-out |*)
-
-#[global] Instance HVariant : Hvariant E0lt_wf free var.
+#[global] Instance HVariant : Hvariant Epsilon0 free var.
 Proof.
  split; intros; eapply round_decr; eauto.
 Qed.
diff --git a/theories/ordinals/Hydra/Omega2_Small.v b/theories/ordinals/Hydra/Omega2_Small.v
index 8af74ed2..95eac6c8 100644
--- a/theories/ordinals/Hydra/Omega2_Small.v
+++ b/theories/ordinals/Hydra/Omega2_Small.v
@@ -21,7 +21,7 @@ Section Impossibility_Proof.
   
   Variable m : Hydra -> ON_Omega2.t.
   Context
-    (Hvar: Hvariant (ON_Generic.ON_wf (ON:=Omega2)) free m).
+    (Hvar: Hvariant Omega2 free m).
 
   (* end snippet Impossibilitya *)
 
diff --git a/theories/ordinals/Hydra/Omega_Small.v b/theories/ordinals/Hydra/Omega_Small.v
index 7470346a..602f232f 100644
--- a/theories/ordinals/Hydra/Omega_Small.v
+++ b/theories/ordinals/Hydra/Omega_Small.v
@@ -3,12 +3,10 @@
 
 
 From Coq Require Import   Arith Lia.
-From hydras Require Import Hydra_Lemmas.
+From hydras Require Import Hydra_Lemmas ON_Generic ON_Omega.
 Open Scope nat_scope.
 
-
-
-#[ global ] Instance height_var : @Hvariant  _ _ lt_wf free height.
+#[global] Instance height_var : Hvariant Omega free height.
 Proof.
   split;intros.
 (*
@@ -28,7 +26,7 @@ Proof.
 Abort.
 (* end show *)
 
-Lemma height_bad :  ~ @Hvariant _ _ lt_wf free height.
+Lemma height_bad :  ~ Hvariant Omega free height.
 Proof.
   intros [H];
   specialize (H 1 (hyd1 (hyd2 head head))  (hyd1 (hyd1 head)));
@@ -51,7 +49,7 @@ Section Impossibility_Proof.
       for proving the termination of all hydra battles *)
  
   Variable m : Hydra -> nat.
-  Context (Hvar : @Hvariant _ _ lt_wf free m).
+  Context (Hvar : Hvariant lt_wf free m).
   
 (* end snippet omegaSmalla *)
   
diff --git a/theories/ordinals/OrdinalNotations/ON_Generic.v b/theories/ordinals/OrdinalNotations/ON_Generic.v
index a9b5a8c5..47a92846 100644
--- a/theories/ordinals/OrdinalNotations/ON_Generic.v
+++ b/theories/ordinals/OrdinalNotations/ON_Generic.v
@@ -24,9 +24,11 @@ Delimit Scope ON_scope with on.
 Class ON {A:Type} (lt: relation A) (cmp: Compare A) :=
   {
   ON_comp :> Comparable lt cmp;
-  ON_wf : well_founded lt;
+  ON_wf :> well_founded lt;
   }.
 #[global] Existing Instance ON_comp.
+Coercion ON_wf :  ON >-> well_founded.
+
 (* end snippet ONDef *)
 
 (* begin snippet ONDefsa:: no-out  *)