From ffb4649ac23ad3fad7dc1d9f4857e129d1dd565a Mon Sep 17 00:00:00 2001
From: Pierre Casteran <pierre.casteran@labri.fr>
Date: Tue, 17 May 2022 17:37:38 +0200
Subject: [PATCH 01/11] Revision book to page 82. deprecate a few symbols

---
 doc/epsilon0-chapter.tex                      | 14 ++--
 doc/ks-chapter.tex                            |  2 +-
 doc/ordinal-chapter.tex                       |  7 +-
 theories/gaia/GCanon.v                        | 14 ++--
 theories/gaia/GF_alpha.v                      |  2 +-
 theories/gaia/GPaths.v                        |  2 +-
 theories/gaia/T1Bridge.v                      |  4 +-
 theories/ordinals/Epsilon0/Canon.v            | 49 +++++------
 theories/ordinals/Epsilon0/E0.v               | 30 +++----
 theories/ordinals/Epsilon0/F_alpha.v          |  8 +-
 theories/ordinals/Epsilon0/Hprime.v           | 10 +--
 theories/ordinals/Epsilon0/L_alpha.v          |  4 +-
 theories/ordinals/Epsilon0/Large_Sets.v       |  8 +-
 theories/ordinals/Epsilon0/Paths.v            | 30 +++----
 theories/ordinals/Epsilon0/T1.v               | 81 ++++++++++---------
 theories/ordinals/Hydra/O2H.v                 | 18 ++---
 .../ordinals/OrdinalNotations/ON_Generic.v    | 12 ++-
 .../ordinals/OrdinalNotations/ON_Omega2.v     |  7 +-
 .../OrdinalNotations/ON_Omega_plus_omega.v    |  6 +-
 .../ordinals/OrdinalNotations/OmegaOmega.v    |  6 +-
 theories/ordinals/solutions_exercises/F_3.v   |  2 +-
 .../solutions_exercises/Limit_Infinity.v      |  6 +-
 22 files changed, 162 insertions(+), 160 deletions(-)

diff --git a/doc/epsilon0-chapter.tex b/doc/epsilon0-chapter.tex
index 7fca16c0..1b0940de 100644
--- a/doc/epsilon0-chapter.tex
+++ b/doc/epsilon0-chapter.tex
@@ -353,9 +353,7 @@ \subsubsection{A Predicate for Characterizing Normal Forms}
 \input{movies/snippets/T1/badTerm}
 
 
-This term would have been written \(\omega^1\times 2 + \omega^\omega \times 3\) in the usual mathematical notation. We note that the exponents of $\omega$ are not in the right (strictly decreasing) order.
-Nevertheless, with the help of the order \texttt{lt} on \texttt{T1}, we are now able to characterize
-the set of all well-formed ordinal terms:
+This term would have been written \(\omega^1\times 2 + \omega^\omega \times 3\) in the usual mathematical notation. We note that the exponents of $\omega$ are not in the right (strictly decreasing) order. The following boolean function determines whether a given ordinal term is well formed.
 
 
 \vspace{4pt}
@@ -472,7 +470,7 @@ \subsubsection{\texttt{E0}: a sigma-type for \texorpdfstring{$\epsilon_0$}{epsil
 
 \paragraph*{\gaiasign}
 \index{gaiabridge}{Type of well formed ordinal terms below $\epsilon_0$}
- The library~\href{../theories/html/gaia_hydras.T1Bridge.html}{gaia\_hydras.T1Bridge} defines a \gaia-compatible type \texttt{E0}.
+ Our library~\href{../theories/html/gaia_hydras.T1Bridge.html}{gaia\_hydras.T1Bridge} defines also a type \texttt{E0} (which doesn't exist in \gaia-\texttt{ssete9}). 
 
 
 
@@ -483,7 +481,7 @@ \subsection{Syntactic definition of limit and successor ordinals}
 
 \vspace{4pt}
 \noindent
-\emph{From Module~\href{../theories/html/hydras.Epsilon0.T1.html\#succb}{Epsilon0.T1}}
+\emph{From Module~\href{../theories/html/hydras.Epsilon0.T1.html\#T1is_succ}{Epsilon0.T1}}
 
 
 
@@ -499,7 +497,7 @@ \subsection{Syntactic definition of limit and successor ordinals}
 
 \paragraph*{\gaiasign}
 \index{gaiabridge}{Limit and successor ordinals}
-In \gaia, the boolean functions associated with limit and successor ordinals are called \texttt{T1limit} and \texttt{T1is\_succ}.
+In \gaia, the boolean functions associated with limit and successor ordinals are also called \texttt{T1limit} and \texttt{T1is\_succ}.
 
  From~\href{../theories/html/gaia_hydras.HydraGaia_Examples.html}{gaia\_hydras.HydraGaia\_Examples}.
 
@@ -527,14 +525,14 @@ \subsubsection{Successor}
 \input{movies/snippets/T1/succDef}
 
 The following lemma establishes the connection between the  function
-\texttt{succ} and the Boolean predicate \texttt{succb}.
+\texttt{succ} and the Boolean predicate \texttt{T1is\_succ}.
 
 \vspace{4pt}
 
 \input{movies/snippets/T1/succbIff}
 
 \begin{exercise}[\gaiasign]
-  Look for the \gaia-theorem which corresponds to \texttt{succb\_iff}.
+  Look for the \gaia-theorem which corresponds to \texttt{T1is\_succ\_iff}.
 \end{exercise}
 
 \subsubsection{Successor function on \texttt{E0}}
diff --git a/doc/ks-chapter.tex b/doc/ks-chapter.tex
index 8da601be..e419cd52 100644
--- a/doc/ks-chapter.tex
+++ b/doc/ks-chapter.tex
@@ -196,7 +196,7 @@ \subsubsection{Limit ordinals are truly limits}
 
 
 Note the use of \coq's \texttt{sig} type in the theorem's statement, which
-relates the boolean function \texttt{limitb} defined on the \texttt{T1} data-type with a constructive view of the limit of a sequence: for any $\beta<\lambda$, we can compute an item of the canonical sequence of $\lambda$ which is greater than $\beta$.
+relates the boolean function \texttt{T1limit} defined on the \texttt{T1} data-type with a constructive view of the limit of a sequence: for any $\beta<\lambda$, we can compute an item of the canonical sequence of $\lambda$ which is greater than $\beta$.
 We can also state directly that $\lambda$ is a (strict) least upper bound of the elements of its canonical sequence.
 
 \input{movies/snippets/Canon/canonSLimitLub}
diff --git a/doc/ordinal-chapter.tex b/doc/ordinal-chapter.tex
index 0058bae9..b24220fd 100644
--- a/doc/ordinal-chapter.tex
+++ b/doc/ordinal-chapter.tex
@@ -952,14 +952,11 @@ \section{Comparing two ordinal notations}
    \label{fig:subsegment}
  \end{figure}
 
-If \texttt{OB} is presumed to be correct, then we may consider that \texttt{OA} ``inherits'' its correctness from the bigger notation system \texttt{OB}.
-
-
 \label{types:SubON}
 \index{hydras}{Library OrdinalNotations!Type classes!SubON}
 
-following definition
-(in ~\href{../theories/html/hydras.OrdinalNotations.ON_Generic.html}{ON\_Generic}).
+\noindent
+From~\href{../theories/html/hydras.OrdinalNotations.ON_Generic.html}{ON\_Generic}.
 
 \input{movies/snippets/ON_Generic/SubONDef}
 
diff --git a/theories/gaia/GCanon.v b/theories/gaia/GCanon.v
index 819ae0e3..6c04f5ce 100644
--- a/theories/gaia/GCanon.v
+++ b/theories/gaia/GCanon.v
@@ -118,9 +118,9 @@ Lemma limit_canonS_not_zero i lambda:
 Proof.
   rewrite -(h2g_g2hK lambda) /canon => Hnf Hlim .
   change zero with (h2g T1.zero); rewrite h2g_eqE. 
-  apply Canon.limitb_canonS_not_zero. 
+  apply Canon.T1limit_canonS_not_zero. 
   - move: Hnf; by rewrite g2h_h2gK -nf_ref.  
-  - by rewrite limitb_ref h2g_g2hK. 
+  - by rewrite T1limit_ref h2g_g2hK. 
 Qed.
 
 
@@ -165,7 +165,7 @@ Proof.
   have H: hcanon (T1.phi0 (g2h lambda)) i = T1.phi0 (hcanon (g2h lambda) i).
   { rewrite -Canon.canon_lim1 => //. 
     - move: Hnf; by rewrite hnf_g2h.
-    - by rewrite limitb_ref h2g_g2hK.
+    - by rewrite T1limit_ref h2g_g2hK.
   }
   by rewrite phi0_ref H.
 Qed. 
@@ -199,7 +199,7 @@ Proof.
   -  congr T1.cons.
   - by rewrite -g2h_canon. 
   - by rewrite hnf_g2h. 
-  - by rewrite limitb_ref h2g_g2hK. 
+  - by rewrite T1limit_ref h2g_g2hK. 
 Qed.
 
 (* begin snippet gCanonLim3:: no-out *)
@@ -211,7 +211,7 @@ Proof.
   rewrite -g2h_eqE g2h_canon !g2h_cons canon_lim3. 
   by rewrite -g2h_canon. 
   1,2 : by rewrite hnf_g2h.   
-  by rewrite limitb_ref h2g_g2hK.
+  by rewrite T1limit_ref h2g_g2hK.
 Qed.
 
 
@@ -223,7 +223,7 @@ Lemma canon_limit_strong lambda :
 (* end snippet gcanonLimitStrong *)
 Proof.
   rewrite -(h2g_g2hK lambda)  -nf_ref
-          -limitb_ref => Hnf Hlim b Hb.
+          -T1limit_ref => Hnf Hlim b Hb.
   rewrite -(h2g_g2hK b) => Hblt; apply hlt_iff in Hblt.
   case (@canon_limit_strong (g2h lambda) Hnf Hlim (g2h b)).
   - split => //; rewrite hnf_g2h => //.
@@ -262,7 +262,7 @@ Lemma  canon_limit_mono lambda i j (Hnf : T1nf lambda)
    rewrite /canon -hlt_iff. 
    case (@canon_limit_mono (g2h lambda)  i j) => //.
    - by rewrite hnf_g2h. 
-   - by  rewrite limitb_ref h2g_g2hK.
+   - by  rewrite T1limit_ref h2g_g2hK.
    - by apply /ltP . 
    -  move => _; case => //.
  Qed. 
diff --git a/theories/gaia/GF_alpha.v b/theories/gaia/GF_alpha.v
index 0d41cb33..d5aab75d 100644
--- a/theories/gaia/GF_alpha.v
+++ b/theories/gaia/GF_alpha.v
@@ -111,7 +111,7 @@ Lemma F_limE alpha i:
 Proof. 
  move => Hlimit; rewrite /F_ F_lim_eqn.
  -  congr hF_; apply E0_eq_intro; cbn; by rewrite g2h_canon. 
- -  rewrite /hE0limit limitb_ref.
+ -  rewrite /hE0limit T1limit_ref.
    move: alpha Hlimit ;case => /= x Hx H'x;  by rewrite h2g_g2hK. 
 Qed.
 
diff --git a/theories/gaia/GPaths.v b/theories/gaia/GPaths.v
index 6bf3bc84..4c0a4de6 100644
--- a/theories/gaia/GPaths.v
+++ b/theories/gaia/GPaths.v
@@ -179,7 +179,7 @@ Theorem KS_thm_2_4 (lambda : T1) :
 (* end snippet KSThm24 *)
 Proof. 
   rewrite -hnf_g2h => Hlambda Hlim i j Hij. 
-  move: Hlim; rewrite -(h2g_g2hK lambda) -limitb_ref => Hlim. 
+  move: Hlim; rewrite -(h2g_g2hK lambda) -T1limit_ref => Hlim. 
   have H'ij: (i < j)%coq_nat by apply /ltP. 
   generalize (KS_thm_2_4 Hlambda Hlim H'ij). 
   by rewrite /const_path !g2h_canon !h2g_g2hK. 
diff --git a/theories/gaia/T1Bridge.v b/theories/gaia/T1Bridge.v
index bdf496e3..ec403db3 100644
--- a/theories/gaia/T1Bridge.v
+++ b/theories/gaia/T1Bridge.v
@@ -454,7 +454,7 @@ Qed.
 (** Limits, successors, etc *)
 
 (* begin snippet limitbRef:: no-out *)
-Lemma limitb_ref (a:Epsilon0.T1.T1) : T1.limitb a = T1limit (h2g a).
+Lemma T1limit_ref (a:Epsilon0.T1.T1) : T1.T1limit a = T1limit (h2g a).
 (* end snippet limitbRef *)
 Proof.
   elim: a => /= //.
@@ -464,7 +464,7 @@ Proof.
 Qed.
 
 (* begin snippet isSuccRef:: no-out *)
-Lemma succb_ref (a:Epsilon0.T1.T1) : T1.succb a = T1is_succ (h2g a).
+Lemma T1is_succ_ref (a:Epsilon0.T1.T1): T1.T1is_succ a = T1is_succ (h2g a).
 (* end snippet isSuccRef *)
 Proof. 
   elim: a => /= //.
diff --git a/theories/ordinals/Epsilon0/Canon.v b/theories/ordinals/Epsilon0/Canon.v
index be7887a2..fc7ee7a8 100644
--- a/theories/ordinals/Epsilon0/Canon.v
+++ b/theories/ordinals/Epsilon0/Canon.v
@@ -114,9 +114,10 @@ Proof.
 Qed.
 
 
-Lemma canonS_lim1 : forall i lambda, nf lambda -> limitb lambda 
-                                 -> canon (cons lambda 0 zero) (S i) =
-                                    T1.phi0 (canon lambda (S i)).
+Lemma canonS_lim1 : forall i lambda,
+    nf lambda -> T1limit lambda 
+    -> canon (cons lambda 0 zero) (S i) =
+         T1.phi0 (canon lambda (S i)).
 Proof.
   intros; unfold canon at 1;  destruct lambda.
   -  discriminate.
@@ -125,7 +126,7 @@ Proof.
      + rewrite pred_of_limit;auto.
 Qed.
 
-Lemma canon_lim1 : forall i lambda, nf lambda -> limitb lambda 
+Lemma canon_lim1 : forall i lambda, nf lambda -> T1limit lambda 
                                     -> canon (cons lambda 0 zero)  i =
                                        T1.phi0 (canon lambda i).
 Proof.
@@ -143,7 +144,7 @@ Qed.
 (** Here *)
 
 Lemma canonS_lim2  i n lambda: 
-    nf lambda -> limitb lambda 
+    nf lambda -> T1limit lambda 
     -> canon (cons lambda (S n) zero) (S i) =
        cons  lambda n (T1.phi0 (canon lambda (S i))).
 Proof.
@@ -156,7 +157,7 @@ Proof.
 Qed.
 
 Lemma canon0_lim2   n lambda: 
-    nf lambda -> limitb lambda 
+    nf lambda -> T1limit lambda 
     -> canon (cons lambda (S n) zero) 0 =
        cons  lambda n (T1.phi0 (canon lambda 0)).
 Proof.
@@ -167,7 +168,7 @@ Proof.
 Qed.
 
 Lemma canon_lim2  i  n lambda : 
-    nf lambda -> limitb lambda 
+    nf lambda -> T1limit lambda 
     -> canon (cons lambda (S n) zero) i =
        cons  lambda n (T1.phi0 (canon lambda i)).
 Proof.
@@ -178,7 +179,7 @@ Qed.
 
 
 Lemma canon_lim3 i n alpha lambda :
-  nf alpha -> nf lambda -> limitb lambda ->
+  nf alpha -> nf lambda -> T1limit lambda ->
   canon (cons alpha n lambda) i = cons alpha n (canon lambda i).
   Proof. 
   simpl (canon (cons alpha n lambda)).
@@ -631,8 +632,8 @@ Qed.
 (** ** Canonical sequences of limit ordinals *)
 
 
-Lemma limitb_canonS_not_zero i lambda:
-  nf lambda -> limitb lambda  -> canon lambda (S i) <> zero.
+Lemma T1limit_canonS_not_zero i lambda:
+  nf lambda -> T1limit lambda  -> canon lambda (S i) <> zero.
 Proof.
   destruct lambda as [ | alpha1 n alpha2].
   - discriminate.
@@ -665,7 +666,7 @@ limit of its  own canonical sequence
 (*| .. coq:: no-out *)
 Lemma canonS_limit_strong lambda : 
   nf lambda ->
-  limitb lambda  ->
+  T1limit lambda  ->
   forall beta, beta t1< lambda ->
                {i:nat | beta t1< canon lambda (S i)}.
 Proof.
@@ -681,12 +682,12 @@ Proof.
       }
       destruct lambda.
       + discriminate.
-      + destruct (T1.limitb_cases Hlambda i).
+      + destruct (T1.T1limit_cases Hlambda i).
        { (* first case : beta = zero *)
         destruct a; subst lambda2; destruct beta.
         { exists 0; apply not_zero_lt. 
           apply nf_canon; auto.
-          apply limitb_canonS_not_zero;auto.
+          apply T1limit_canonS_not_zero;auto.
         }
         destruct (LT_inv_strong H1).
         * destruct n.
@@ -787,7 +788,7 @@ Proof.
       destruct beta.
        * exists 0;  apply not_zero_lt.
          apply nf_canon; trivial; auto with T1.
-         apply limitb_canonS_not_zero; trivial. 
+         apply T1limit_canonS_not_zero; trivial. 
        *  destruct (LT_inv_strong H1).
           -- exists 0;  rewrite canon_tail.
              apply LT2;auto.
@@ -834,14 +835,14 @@ Proof.
       }
       all: auto. 
   -   destruct s as [t [Ht Ht']]; subst lambda.
-      destruct (@limitb_succ t); auto.
+      destruct (@T1limit_succ t); auto.
       (*||*)
 Defined.
       (* end snippet canonSLimitStrong *)
 
 Lemma canon_limit_strong lambda : 
   nf lambda ->
-  limitb lambda  ->
+  T1limit lambda  ->
   forall beta, beta t1< lambda ->
                 {i:nat | beta t1< canon lambda i}.
 Proof.
@@ -852,7 +853,7 @@ Defined.
 (* begin snippet canonSLimitLub *)
 
 Lemma canonS_limit_lub (lambda : T1) :
-  nf lambda -> limitb lambda  -> strict_lub (canonS lambda) lambda. (* .no-out *) (*| .. coq:: none |*)
+  nf lambda -> T1limit lambda  -> strict_lub (canonS lambda) lambda. (* .no-out *) (*| .. coq:: none |*)
 Proof.
   split.
   - intros; split.
@@ -878,7 +879,7 @@ Qed.
 (* end snippet canonSLimitLub *)
 
 
-Lemma canon_limit_mono alpha i j : nf alpha -> limitb alpha  ->
+Lemma canon_limit_mono alpha i j : nf alpha -> T1limit alpha  ->
                                     i < j ->
                                     canon alpha i t1< canon alpha j.
 Proof. 
@@ -886,9 +887,9 @@ Proof.
   clear alpha;  intros alpha Hrec alpha_nf Hlim Hij. 
    destruct alpha. 
   - discriminate. 
-  -  destruct (@T1.limitb_cases _ _ _ alpha_nf Hlim) as [[H1 H2] | H3].
+  -  destruct (@T1.T1limit_cases _ _ _ alpha_nf Hlim) as [[H1 H2] | H3].
      +  subst; destruct n. 
-        * case_eq (limitb alpha1). 
+        * case_eq (T1limit alpha1). 
           -- intro H; repeat rewrite canon_lim1; auto. 
              ++ apply phi0_mono_strict_LT, Hrec; auto. 
                 apply lt_a_phi0_a.
@@ -946,12 +947,12 @@ Proof.
            --  apply nf_tail_lt with alpha2; auto. 
                apply canon_LT; auto.
                ++ eapply nf_inv2; eassumption. 
-               ++  apply limitb_not_zero; auto. 
+               ++  apply T1limit_not_zero; auto. 
                    eapply nf_inv2; eassumption.
            --  apply nf_tail_lt with alpha2; auto. 
                apply canon_LT; auto.
                eapply nf_inv2; eassumption. 
-               apply limitb_not_zero; auto. 
+               apply T1limit_not_zero; auto. 
                eapply nf_inv2; eassumption.
            -- apply Hrec; auto. 
               eapply nf_inv2; eauto.
@@ -965,7 +966,7 @@ Qed.
 
 
 
-Lemma canonS_limit_mono alpha i j : nf alpha -> limitb alpha  ->
+Lemma canonS_limit_mono alpha i j : nf alpha -> T1limit alpha  ->
                                     i < j ->
                                     canonS alpha i t1< canonS alpha j.
 Proof. 
@@ -1104,7 +1105,7 @@ Lemma Canon_of_limit_not_null : forall i alpha, E0limit alpha ->
                                        Canon alpha (S i) <> E0zero.
 Proof.
   destruct alpha;simpl;unfold CanonS; simpl;  rewrite E0_eq_iff.
-  simpl;   apply limitb_canonS_not_zero; auto.
+  simpl;   apply T1limit_canonS_not_zero; auto.
 Qed.
 
 Global Hint Resolve CanonS_lt Canon_lt Canon_of_limit_not_null : E0.
diff --git a/theories/ordinals/Epsilon0/E0.v b/theories/ordinals/Epsilon0/E0.v
index bdbad61d..0f941bd1 100644
--- a/theories/ordinals/Epsilon0/E0.v
+++ b/theories/ordinals/Epsilon0/E0.v
@@ -72,13 +72,13 @@ Next Obligation.  apply succ_nf, cnf_ok. Defined.
 #[deprecated(note="use E0succ")]
  Notation Succ := E0succ (only parsing).
 
-Definition E0limit (alpha : E0) : bool :=  limitb (@cnf alpha).
+Definition E0limit (alpha : E0) : bool :=  T1limit (@cnf alpha).
 
 #[deprecated(note="use E0limit")]
  Notation Limitb := E0limit (only parsing).
 
 Definition E0is_succ (alpha : E0) : bool :=
-  succb (@cnf alpha).
+  T1is_succ (@cnf alpha).
 
 #[deprecated(note="use E0is_succ")]
  Notation E0succb := E0is_succ (only parsing).
@@ -223,7 +223,7 @@ Qed.
 Lemma Succb_Succ alpha : E0is_succ alpha -> {beta : E0 | alpha = E0succ beta}.
 Proof.
   destruct alpha; cbn.
-  intro H; destruct (succb_def cnf_ok0 H) as [beta [Hbeta Hbeta']]; subst.
+  intro H; destruct (T1is_succ_def cnf_ok0 H) as [beta [Hbeta Hbeta']]; subst.
   assert (nf (succ beta)) by eauto with T1.
   exists (@mkord  beta Hbeta); apply E0_eq_intro; now cbn.
 Defined.
@@ -268,7 +268,7 @@ Lemma cnf_Omega_term (alpha: E0) (n: nat) :
   cnf (Omega_term alpha n) = omega_term (cnf alpha) n.
 Proof. reflexivity. Defined.
 
-Lemma Limitb_Omega_term alpha i : alpha <> E0zero ->
+Lemma T1limit_Omega_term alpha i : alpha <> E0zero ->
                                   E0limit (Omega_term alpha i).
 Proof.
   intro H; unfold E0limit; destruct alpha as [cnf0 H0]; cbn;
@@ -277,13 +277,13 @@ Proof.
   - red; trivial. 
 Qed.
 
-Lemma Limitb_phi0 alpha  : alpha <> E0zero ->
+Lemma T1limit_phi0 alpha  : alpha <> E0zero ->
                            E0limit (E0phi0 alpha).
 Proof.
-  unfold E0phi0; apply Limitb_Omega_term.
+  unfold E0phi0; apply T1limit_Omega_term.
 Qed.
 
-#[global] Hint Resolve Limitb_phi0 : E0.
+#[global] Hint Resolve T1limit_phi0 : E0.
 
 Definition Zero_Limit_Succ_dec (alpha : E0) :
   {alpha = E0zero} + {E0limit alpha = true} +
@@ -365,8 +365,8 @@ Proof.
   destruct s.
   - unfold E0succ, E0zero in e; injection  e .
     intro H; now   destruct (T1.succ_not_zero (cnf alpha)).
-  -  unfold limitb, E0succ in e; simpl in e;
-       destruct (@T1.limitb_succ (cnf alpha)); auto.
+  -  unfold T1limit, E0succ in e; simpl in e;
+       destruct (@T1.T1limit_succ (cnf alpha)); auto.
         destruct alpha; simpl; auto. 
   -  destruct s.
     { unfold E0succ in e;  injection e.
@@ -401,7 +401,7 @@ Global Hint Resolve E0pred_Lt : E0.
 
 
 Lemma Succ_Succb (alpha : E0) : E0is_succ (E0succ alpha).
-destruct alpha; unfold E0is_succ, E0succ; cbn; apply T1.succ_succb.
+destruct alpha; unfold E0is_succ, E0succ; cbn; apply T1.succ_is_succ.
 Qed.
 
 Global Hint Resolve Succ_Succb : E0.
@@ -429,7 +429,7 @@ Hint Rewrite FinS_Succ_eq : E0_rw.
 Lemma Limit_not_Zero alpha : E0limit alpha -> alpha <> E0zero.
 Proof.
   destruct alpha; unfold E0limit, E0zero; cbn; intros H H0.
-  injection H0;  intro ; subst cnf0; eapply T1.limitb_not_zero; eauto.
+  injection H0;  intro ; subst cnf0; eapply T1.T1limit_not_zero; eauto.
 Qed.
 
 
@@ -445,13 +445,13 @@ Proof.
 Qed.
 
 
-Lemma Succ_not_Limitb alpha : E0is_succ alpha -> ~ E0limit alpha .
+Lemma Succ_not_T1limit alpha : E0is_succ alpha -> ~ E0limit alpha .
 Proof. 
   red; destruct alpha; unfold E0is_succ, E0limit; cbn.
   intros H H0. rewrite (succ_not_limit _ H) in H0. discriminate.  
 Qed.
 
-Global Hint Resolve Limit_not_Zero Succ_not_Zero Lt_Succ Succ_not_Limitb : E0.
+Global Hint Resolve Limit_not_Zero Succ_not_Zero Lt_Succ Succ_not_T1limit : E0.
 
 Lemma lt_Succ_inv : forall alpha beta, beta o< alpha <->
                                        E0succ beta o<= alpha.
@@ -470,7 +470,7 @@ Proof.
  cbn;  apply LT_succ_LE_2; auto.
 Qed.
 
-Lemma Succ_lt_Limitb alpha beta:
+Lemma Succ_lt_T1limit alpha beta:
     E0limit alpha ->  beta o< alpha -> E0succ beta o< alpha.
 Proof.
   destruct alpha, beta;unfold E0lt; cbn.
@@ -612,7 +612,7 @@ Proof.
   intros. unfold Cons. rewrite Omega_term_plus; auto.
 Defined.
 
-Lemma Limitb_plus alpha beta i:
+Lemma T1limit_plus alpha beta i:
   (beta o< E0phi0 alpha)%e0 -> E0limit beta ->
   E0limit  (Omega_term alpha i + beta)%e0.
 Proof.
diff --git a/theories/ordinals/Epsilon0/F_alpha.v b/theories/ordinals/Epsilon0/F_alpha.v
index d40e271d..f149983c 100644
--- a/theories/ordinals/Epsilon0/F_alpha.v
+++ b/theories/ordinals/Epsilon0/F_alpha.v
@@ -123,7 +123,7 @@ Proof.
   - subst alpha; discriminate H.
   - cbn; destruct (Utils.dec (E0limit alpha)) .
     + assert (true=false) by 
-          ( now  destruct (Succ_not_Limitb _ H)). 
+          ( now  destruct (Succ_not_T1limit _ H)). 
       discriminate.
     + now cbn.
 Qed.
@@ -779,10 +779,10 @@ Section H'_F.
               ** destruct alpha; auto.
               ** auto with arith. 
           --  apply nf_canon, cnf_ok.
-          --  apply limitb_canonS_not_zero.
+          --  apply T1limit_canonS_not_zero.
               ++ apply cnf_ok.
               ++ now destruct alpha.
-    - apply Limitb_phi0.
+    - apply T1limit_phi0.
       apply Limit_not_Zero; auto. 
 Qed.
 
@@ -867,7 +867,7 @@ Proof.
   - subst alpha; discriminate H.
   - cbn; destruct (Utils.dec (E0limit alpha)) .
     + assert (true=false) by 
-          ( now  destruct (Succ_not_Limitb _ H)). 
+          ( now  destruct (Succ_not_T1limit _ H)). 
       discriminate.
     + now cbn.
 Qed.
diff --git a/theories/ordinals/Epsilon0/Hprime.v b/theories/ordinals/Epsilon0/Hprime.v
index 871d02ac..28160611 100644
--- a/theories/ordinals/Epsilon0/Hprime.v
+++ b/theories/ordinals/Epsilon0/Hprime.v
@@ -66,7 +66,7 @@ Proof.
   destruct (E0_eq_dec alpha E0zero).
   - subst; discriminate.
   - cbn;  destruct (Utils.dec (E0limit alpha)) .
-    destruct (Succ_not_Limitb _ H); auto.
+    destruct (Succ_not_T1limit _ H); auto.
     + now cbn.
 Qed.
 
@@ -254,7 +254,7 @@ Proof with auto with E0.
        assert (CanonS beta k o< beta)%e0 by auto with E0.
        assert (CanonS beta k o< E0phi0 alpha)%e0 by (eapply Lt_trans; eauto).
        now rewrite (Hbeta H1 H2 k), (H'_eq3 beta).
-       apply Limitb_plus; auto.
+       apply T1limit_plus; auto.
      +   intro k; destruct s as [gamma Hgamma]; subst.
          specialize (Hbeta gamma).
          assert (gamma o< E0succ gamma)%e0 by (apply Lt_Succ; auto).
@@ -290,7 +290,7 @@ Proof with auto with E0.
              unfold Omega_term; simpl. unfold canonS.
              destruct (cnf alpha) ...
              destruct (pred (cons t1 n t2)) ...
--   unfold canonS; apply Limitb_Omega_term ...
+-   unfold canonS; apply T1limit_Omega_term ...
 Qed.
 
 End H'_cons.
@@ -703,7 +703,7 @@ Section Proof_of_Abstract_Properties.
         -  apply Canon_lt;  now apply Limit_not_Zero.
         -  eapply PB0; intro H.
            assert (H0 :cnf (Canon alpha (S n)) = cnf E0zero) by (f_equal; auto).
-           simpl in H0;   apply (@limitb_canonS_not_zero n (cnf alpha)); auto.
+           simpl in H0;   apply (@T1limit_canonS_not_zero n (cnf alpha)); auto.
            +  apply cnf_ok.
       Qed.
 
@@ -913,7 +913,7 @@ Section Proof_of_H'_mono_l.
     Hypothesis Hbeta: E0limit beta.
 
     Remark R4 : E0succ alpha o< beta.
-    Proof. now apply Succ_lt_Limitb. Qed.
+    Proof. now apply Succ_lt_T1limit. Qed.
 
     Remark R5 :  {n: nat | forall p, n <= p ->
                                      H'_ alpha (S p) < H'_ beta (S p)}.
diff --git a/theories/ordinals/Epsilon0/L_alpha.v b/theories/ordinals/Epsilon0/L_alpha.v
index 0eae5cf7..e7271ba9 100644
--- a/theories/ordinals/Epsilon0/L_alpha.v
+++ b/theories/ordinals/Epsilon0/L_alpha.v
@@ -53,7 +53,7 @@ Proof.
   intros; rewrite L__equation_1;  destruct (E0_eq_dec alpha E0zero).
   - subst; discriminate.
   - cbn; destruct (Utils.dec (E0limit alpha)) .
-    apply Succ_not_Limitb in H; destruct H; auto.
+    apply Succ_not_T1limit in H; destruct H; auto.
     now cbn.
 Qed.
 
@@ -200,7 +200,7 @@ Section L_correct_proof.
     unfold P; intros.
     apply L_spec_compat with (fun k =>  L_ (Canon alpha k) (S k)).
     -   generalize L_lim_ok; intro H1; unfold L_lim in H1.
-       assert (H2 : limitb (cnf alpha)) by (now destruct alpha). 
+       assert (H2 : T1limit (cnf alpha)) by (now destruct alpha). 
        specialize (H1 (cnf alpha) cnf_ok H2 (fun k i => L_ (Canon alpha k) i)).
        apply H1; intro k; specialize (H (Canon alpha  (S k))).
        assert  (H3: (Canon alpha (S k) o< alpha)%e0 ).
diff --git a/theories/ordinals/Epsilon0/Large_Sets.v b/theories/ordinals/Epsilon0/Large_Sets.v
index c10ff022..354d412e 100644
--- a/theories/ordinals/Epsilon0/Large_Sets.v
+++ b/theories/ordinals/Epsilon0/Large_Sets.v
@@ -329,14 +329,14 @@ End succ.
 Section lim.
   Variables (lambda : T1)
             (Hnf : nf lambda)
-            (Hlim : limitb lambda)
+            (Hlim : T1limit lambda)
             (f : nat -> nat -> nat)
             (H : forall k, L_spec (canon lambda (S k)) (f (S k))).
   
   Remark canon_not_null : forall k,  canon lambda (S k) <> zero.
   (*| .. coq:: none |*)
   Proof.
-   intro; apply limitb_canonS_not_zero; auto.  
+   intro; apply T1limit_canonS_not_zero; auto.  
   Qed.
   (*||*)
   
@@ -346,7 +346,7 @@ Section lim.
   (*| .. coq:: none |*)
   Proof.
     right.
-    - apply limitb_not_zero; auto.
+    - apply T1limit_not_zero; auto.
     - intro k;  unfold L_lim.  red; path_decompose (S k).
       instantiate (1:= canon lambda (S k)).
       *  specialize (H k); inversion H.
@@ -355,7 +355,7 @@ Section lim.
       * rewrite interval_singleton; left.
        --    discriminate.
        -- split.
-        ++  apply limitb_not_zero; auto.
+        ++  apply T1limit_not_zero; auto.
         ++  reflexivity.
      *  specialize (L_pos_inv (canon lambda (S k)) (f (S k))
                               (canon_not_null k) (H k) (S k));  abstract lia.       
diff --git a/theories/ordinals/Epsilon0/Paths.v b/theories/ordinals/Epsilon0/Paths.v
index e81bfdc1..ab191f9b 100644
--- a/theories/ordinals/Epsilon0/Paths.v
+++ b/theories/ordinals/Epsilon0/Paths.v
@@ -656,7 +656,7 @@ Proof. reflexivity. Qed.
 
 
 Lemma gnawS_lim1 (i:nat)(s: list nat) (lambda : T1) :
-  nf lambda -> limitb lambda ->
+  nf lambda -> T1limit lambda ->
   gnawS (T1.cons lambda 0 T1.zero) (i::s) =
   gnawS (T1.cons (canon lambda (S i)) 0 T1.zero) s.
 Proof.
@@ -666,7 +666,7 @@ Qed.
 
 
 Lemma gnawS_lim2 (i n:nat)(s: list nat) (lambda : T1) :
-  nf lambda -> limitb  lambda->
+  nf lambda -> T1limit  lambda->
   gnawS (T1.cons lambda (S n) T1.zero) (i::s) =
   gnawS (T1.cons lambda n (T1.cons (canon lambda (S i)) 0 T1.zero)) s.
 Proof.
@@ -840,7 +840,7 @@ Proof with eauto with T1.
     destruct  (canonS_limit_strong H1 Hlimit H) as [j Hj].
     destruct (IHalpha (canon alpha (S j))) as [x p]; auto.
     apply canonS_LT; auto.
-    apply limitb_not_zero;auto.
+    apply T1limit_not_zero;auto.
     exists (j::x); eright.
     {split. intro;  subst.
      - inversion  Hlimit.
@@ -1161,7 +1161,7 @@ Proof.
         *  apply hrec.
             -- apply canonS_LT;auto.
             -- eapply nf_canon; eauto. 
-            -- now apply limitb_canonS_not_zero.
+            -- now apply T1limit_canonS_not_zero.
   - destruct s as [beta [Hbeta e]]; subst.
     destruct (T1_eq_dec beta zero).
    + subst;    left; split; auto.  
@@ -1259,7 +1259,7 @@ Proof.
             split;[discriminate | trivial].
           *   apply IHclos_trans_1n.
               apply nf_canon;auto.
-              apply limitb_canonS_not_zero; auto.
+              apply T1limit_canonS_not_zero; auto.
       -  destruct s as [beta [H3 e]]; subst x.
          destruct (T1_eq_dec beta zero).
          { subst beta; destruct (const_pathS_zero H0). }
@@ -1274,7 +1274,7 @@ Qed.
 (*| .. coq:: no-out |*)
 Theorem KS_thm_2_4 (lambda : T1) :
    nf lambda ->
-   limitb lambda  ->
+   T1limit lambda  ->
    forall i j, (i < j)%nat ->
                const_path 1 (canon lambda (S j))
                              (canon lambda (S i)).
@@ -1289,7 +1289,7 @@ Proof.
     + destruct alpha.
       * discriminate.
       *  nf_decomp Halpha.
-         destruct (limitb_cases Halpha  H).
+         destruct (T1limit_cases Halpha  H).
          { destruct a; subst alpha2.
            intros i0 j H1;  destruct (@zero_limit_succ_dec alpha1) ;
              trivial.
@@ -1303,7 +1303,7 @@ Proof.
                split ; trivial.
                apply head_lt_cons ; trivial.
                apply nf_canon ; eauto with T1. 
-               apply limitb_canonS_not_zero ; eauto with T1.
+               apply T1limit_canonS_not_zero ; eauto with T1.
              - repeat rewrite canonS_lim2 ; eauto with T1.
                 apply KS_thm_2_4_lemma1 ; trivial. 
                 apply cons_nf ; trivial. 
@@ -1318,7 +1318,7 @@ Proof.
                 apply  head_lt_cons ; eauto with T1.
                 apply single_nf ; eauto with T1.
                 apply nf_canon ; eauto with T1.
-                apply limitb_canonS_not_zero ; eauto with T1.
+                apply T1limit_canonS_not_zero ; eauto with T1.
            }
            destruct s as [beta [H2 H3]];  subst; clear H i; induction n.
            {
@@ -1339,14 +1339,14 @@ Proof.
          apply KS_thm_2_4_lemma1 ; trivial. 
          apply nf_LT_right with alpha2 ; eauto with T1.
          apply canonS_LT ; eauto with T1.
-         apply limitb_canonS_not_zero ; eauto with T1.
+         apply T1limit_canonS_not_zero ; eauto with T1.
          apply Hrec ; eauto with T1.
          split ; eauto with T1.
          split ; eauto with T1.
          apply  tail_lt_cons; auto.
          all: intro; subst; discriminate.
   -  destruct s as [beta [H0 H1]]; 
-       subst; destruct (@limitb_succ beta); auto.
+       subst; destruct (@T1limit_succ beta); auto.
      (*||*)
 Qed.
 
@@ -1536,7 +1536,7 @@ Proof.
            left.
            split.
            ++ intro e;subst. 
-              destruct (@limitb_not_zero zero) ; auto.
+              destruct (@T1limit_not_zero zero) ; auto.
            ++ reflexivity. 
        -- rewrite  clos_trans_t1n_iff;  apply Cor12_1 with n2; auto.
           auto with arith.  
@@ -1650,7 +1650,7 @@ Proof.
           left.
             split.
             intro;subst.
-           destruct (@limitb_not_zero zero); trivial. 
+           destruct (@T1limit_not_zero zero); trivial. 
            trivial.
           assert (const_pathS  (S p) lambda (T1.succ (canon  lambda (S p)))).
           {
@@ -1696,7 +1696,7 @@ Proof.
           eauto with T1.
           auto.
           
-          (* end of the limitb case *)
+          (* end of the T1limit case *)
           {
             destruct s as [gamma [H1 H2]];destruct (T1_eq_dec gamma zero).
             {
@@ -3004,7 +3004,7 @@ Lemma Canon_mono1 alpha i j : E0limit  alpha -> (i< j)% nat ->
     cbn. auto with T1.
     now apply nf_canon.
     split; cbn. 
-    specialize (limitb_canonS_not_zero j cnf_ok H).
+    specialize (T1limit_canonS_not_zero j cnf_ok H).
     intro.
     
     apply canon_limit_mono; auto. 
diff --git a/theories/ordinals/Epsilon0/T1.v b/theories/ordinals/Epsilon0/T1.v
index 6cca5985..3d0105b1 100644
--- a/theories/ordinals/Epsilon0/T1.v
+++ b/theories/ordinals/Epsilon0/T1.v
@@ -92,28 +92,35 @@ Proof. reflexivity. Qed.
 
 (* begin snippet succbLimitb *)
 
-Fixpoint succb alpha :=
+
+Fixpoint T1is_succ alpha :=
   match alpha with
-      zero => false
+    | zero => false
     | cons zero _ _ => true
-    | cons alpha n beta => succb beta
+    | cons alpha n beta => T1is_succ beta
   end.
+#[deprecated(note="use T1is_succ")]
+ Notation succb := T1is_succ (only parsing).
+
 
-Fixpoint limitb alpha :=
+Fixpoint T1limit alpha :=
   match alpha with
-      zero => false
+    | zero => false
     | cons zero _ _ => false
     | cons alpha n zero => true
-    | cons alpha n beta => limitb beta
+    | cons alpha n beta => T1limit beta
   end.
 
-Compute limitb T1omega.
+#[deprecated(note="use T1limit")]
+  Notation limitb := T1limit (only parsing).
+
+Compute T1limit T1omega.
 
-Compute limitb 42.
+Compute T1limit 42.
 
-Compute succb 42.
+Compute T1is_succ 42.
 
-Compute succb T1omega.
+Compute T1is_succ T1omega.
 
 (* end snippet succbLimitb *)
 
@@ -156,7 +163,7 @@ Inductive ap : T1 -> Prop :=
  *)
 
 (* begin snippet compareDef *)
-#[ global ] Instance compare_T1 : Compare T1 :=
+#[global] Instance compare_T1 : Compare T1 :=
  fix cmp (alpha beta:T1) :=
   match alpha, beta with
   | zero, zero => Eq
@@ -871,7 +878,7 @@ Proof.
   - cbn; destruct alpha1; discriminate.
 Qed.
 
-Lemma succ_succb : forall alpha, succb (succ alpha).
+Lemma succ_is_succ : forall alpha, T1is_succ (succ alpha).
 Proof.
   induction  alpha.
    - reflexivity.
@@ -3398,11 +3405,11 @@ Qed.
 
 
 
-Lemma limitb_cases : forall alpha n beta,
+Lemma T1limit_cases : forall alpha n beta,
     nf (cons alpha n beta) ->
-    limitb (cons alpha n beta)  ->
+    T1limit (cons alpha n beta)  ->
     { alpha <> zero /\ beta = zero} +
-    {alpha <> zero /\ limitb beta }.
+    {alpha <> zero /\ T1limit beta }.
 Proof.
   intros alpha n beta H;  simpl;  destruct alpha.
   - discriminate.
@@ -3447,14 +3454,14 @@ Qed.
 
 
 Lemma pred_of_limit : forall alpha, nf alpha ->
-                                    limitb alpha ->
+                                    T1limit alpha ->
                                     pred alpha = None.
 Proof.
   intros; induction alpha.
   - reflexivity. 
   -    simpl; destruct alpha1.
        +   destruct n;  simpl in H0; discriminate.
-       +   destruct (limitb_cases  H H0).
+       +   destruct (T1limit_cases  H H0).
            *  destruct a.    
               subst.
               reflexivity.
@@ -3465,7 +3472,7 @@ Qed.
 
 Definition zero_limit_succ_dec :
   forall alpha, nf alpha ->
-                ({alpha = zero} + {limitb alpha }) + 
+                ({alpha = zero} + {T1limit alpha }) + 
                 {beta : T1 |  nf beta /\ alpha = succ beta} .
 Proof with eauto with T1.
   induction alpha as [| gamma Hgamma n beta Hbeta].
@@ -3505,7 +3512,7 @@ Defined.
 
 
 Lemma pred_of_limitR : forall alpha, nf alpha -> alpha <> zero ->
-                                     pred alpha = None -> limitb alpha.
+                                     pred alpha = None -> T1limit alpha.
 Proof.
   intros alpha Halpha; destruct (zero_limit_succ_dec Halpha).
   - destruct s; auto.
@@ -3545,7 +3552,7 @@ Qed.
 
 
 
-Lemma limitb_succ : forall alpha, nf alpha ->  ~ limitb (succ alpha) .
+Lemma T1limit_succ : forall alpha, nf alpha ->  ~ T1limit (succ alpha) .
   induction alpha.
   - discriminate.
   - intros;  simpl;  destruct alpha1.
@@ -3562,28 +3569,28 @@ Proof.
   -  now apply succ_nf.
 Qed.
 
-Lemma limitb_not_zero : forall alpha, nf alpha -> limitb alpha  ->
+Lemma T1limit_not_zero : forall alpha, nf alpha -> T1limit alpha  ->
                                         alpha <> zero.
 Proof.
   unfold not; intros; subst;discriminate.
 Qed.
 
 
-Global Hint Resolve limitb_not_zero : T1.
+Global Hint Resolve T1limit_not_zero : T1.
 
 
-Lemma limitb_succ_tail :
-  forall alpha n beta, nf beta ->  ~ limitb (cons alpha n (succ beta)).
+Lemma T1limit_succ_tail :
+  forall alpha n beta, nf beta ->  ~ T1limit (cons alpha n (succ beta)).
 Proof.  
   simpl;intros; destruct alpha.
   - discriminate.
   -  case_eq (succ beta).
      + intro; now destruct (succ_not_zero beta).
-     +  intros gamma p delta H0;  rewrite <- H0; now  apply limitb_succ.
+     +  intros gamma p delta H0;  rewrite <- H0; now  apply T1limit_succ.
 Qed.
 
 
-Lemma succ_not_limit : forall alpha:T1, succb alpha -> limitb alpha = false.
+Lemma succ_not_limit : forall alpha:T1, T1is_succ alpha -> T1limit alpha = false.
 Proof.
   induction  alpha. 
   intro; discriminate.
@@ -3596,8 +3603,8 @@ Proof.
 Qed.
 
 
-Lemma succb_def alpha (Halpha : nf alpha) :
-  succb alpha -> {beta | nf beta /\ alpha = succ  beta}.
+Lemma T1is_succ_def alpha (Halpha : nf alpha) :
+  T1is_succ alpha -> {beta | nf beta /\ alpha = succ  beta}.
 Proof.
   intro H; destruct   (zero_limit_succ_dec Halpha) as [[H0 | H0] | H0].
   - subst alpha; discriminate.
@@ -3607,16 +3614,16 @@ Proof.
 Defined.
 
 (* begin snippet succbIff:: no-out *)
-Lemma succb_iff alpha (Halpha : nf alpha) :
-  succb alpha <->  exists beta : T1,  nf beta /\ alpha = succ  beta.
+Lemma T1is_succ_iff alpha (Halpha : nf alpha) :
+  T1is_succ alpha <->  exists beta : T1,  nf beta /\ alpha = succ  beta.
 (* end snippet succbIff *)
 
 Proof.
   split.
-  - intro H; destruct (succb_def Halpha); [trivial | ].  
+  - intro H; destruct (T1is_succ_def Halpha); [trivial | ].  
      exists x; assumption.
   - destruct 1 as [beta [Hbeta  H'beta]]; subst;   
-      now apply succ_succb.
+      now apply succ_is_succ.
 Qed.
 
 
@@ -3722,8 +3729,8 @@ Qed.
 
 
 
-Lemma strict_lub_limitb : forall (alpha :T1)(s : nat -> T1),
-    nf alpha -> strict_lub s alpha -> limitb alpha.
+Lemma strict_lub_T1limit : forall (alpha :T1)(s : nat -> T1),
+    nf alpha -> strict_lub s alpha -> T1limit alpha.
 Proof.
   destruct 2.
   destruct (zero_limit_succ_dec H).
@@ -3822,13 +3829,13 @@ Qed.
 
 
 
-Lemma succ_lt_limit alpha (Halpha : nf alpha)(H : limitb alpha ):
+Lemma succ_lt_limit alpha (Halpha : nf alpha)(H : T1limit alpha ):
   forall beta, beta t1< alpha -> succ beta t1< alpha.
 Proof. 
   intros beta H0;  assert (H1 :succ beta t1<= alpha) by 
       (apply  LT_succ_LE; auto).
   destruct (LE_LT_eq_dec H1); auto.
-  subst alpha; destruct  (@limitb_succ beta ); eauto with T1. 
+  subst alpha; destruct  (@T1limit_succ beta ); eauto with T1. 
 Qed. 
 
 
@@ -4244,7 +4251,7 @@ Proof. now compute. Qed.
 (* end snippet plusMultExamples *)
 
 
-Example Ex5 : limitb (T1omega ^ (T1omega + 5)).
+Example Ex5 : T1limit (T1omega ^ (T1omega + 5)).
 Proof. reflexivity. Qed.
 
 (* Demo *)
diff --git a/theories/ordinals/Hydra/O2H.v b/theories/ordinals/Hydra/O2H.v
index 68cc93f1..f3433855 100644
--- a/theories/ordinals/Hydra/O2H.v
+++ b/theories/ordinals/Hydra/O2H.v
@@ -95,7 +95,7 @@ Proof.
 Qed.
 
 Lemma iota_rw1 :
-  forall i alpha,  nf alpha -> limitb alpha = true ->
+  forall i alpha,  nf alpha -> T1limit alpha = true ->
                    iota (canonS (cons alpha 0 zero) i) =
                    hyd1 (iota (canonS alpha i)).
 Proof.                        
@@ -103,7 +103,7 @@ Proof.
 Qed.
 
 Lemma iota_rw2 :
-  forall i n alpha,  nf alpha -> limitb alpha = true ->
+  forall i n alpha,  nf alpha -> T1limit alpha = true ->
                      iota (canonS (cons alpha (S n) zero) i) =
                      node (hcons_mult (iota alpha) (S n) 
                                       (hcons
@@ -188,12 +188,12 @@ Proof.
   inversion 1;   eapply S0_mem_head; eauto.
 Qed.
 
-Lemma limit_no_head : forall alpha, nf alpha -> limitb alpha = true ->
+Lemma limit_no_head : forall alpha, nf alpha -> T1limit alpha = true ->
                                     ~ mem_head (iotas alpha).
 Proof. 
   induction alpha.
   - discriminate.
-  - intros; simpl;  destruct (limitb_cases H).
+  - intros; simpl;  destruct (T1limit_cases H).
     +  auto.
     +  destruct a;  subst; intro H2;  inversion H2.
        destruct alpha1.
@@ -219,7 +219,7 @@ Qed.
 
 
 Lemma limit_no_R1 : forall alpha, nf alpha ->
-                                  limitb alpha = true ->
+                                  T1limit alpha = true ->
                                   forall h', ~ R1 (iota alpha) h'.
 Proof.
   intros alpha H H0 h' H1; generalize ( limit_no_head _ H H0).
@@ -275,13 +275,13 @@ Section DS_iota.
   
   Lemma DS_iota_2 : forall lambda,
       nf lambda -> alpha = T1.phi0 lambda ->
-      limitb lambda ->
+      T1limit lambda ->
       round_n i (iota alpha) (iota (canonS alpha i)).                             
   Proof. 
     intros;subst alpha.
     repeat rewrite iota_phi0; trivial.
     assert (nz : lambda <> zero).
-    { eapply limitb_not_zero; eauto. }
+    { eapply T1limit_not_zero; eauto. }
     right;  specialize (Hrec lambda nz (head_LT_cons  Halpha)).
     (* unfold T1.phi0; *) rewrite iota_rw1; trivial.
     right; left;  destruct (Hrec (canonS lambda i)); auto.
@@ -305,7 +305,7 @@ Section DS_iota.
   Section Proof_case_4.
     Variable lambda: T1.
     Hypothesis Hlambda : nf lambda.
-    Hypothesis Hlim : limitb lambda.
+    Hypothesis Hlim : T1limit lambda.
     Variable n : nat.
     Hypothesis Hn : alpha = cons lambda (S n) zero.
 
@@ -322,7 +322,7 @@ Section DS_iota.
       left;  specialize (Hrec lambda).
       assert (lambda t1< cons lambda (S n) zero)%t1.
       {  apply head_LT_cons; auto with T1. }
-      specialize (Hrec (limitb_not_zero Hlambda Hlim)
+      specialize (Hrec (T1limit_not_zero Hlambda Hlim)
                        H  (canonS lambda i) (refl_equal _)).
       destruct Hrec; [| trivial];
         elimtype False;
diff --git a/theories/ordinals/OrdinalNotations/ON_Generic.v b/theories/ordinals/OrdinalNotations/ON_Generic.v
index 7c7cb7a4..62c09f0c 100644
--- a/theories/ordinals/OrdinalNotations/ON_Generic.v
+++ b/theories/ordinals/OrdinalNotations/ON_Generic.v
@@ -87,10 +87,9 @@ Global Hint Resolve wf_measure : core.
 Class  SubON 
        `(OA: @ON A ltA compareA)
        `(OB: @ON B ltB compareB)
-       (alpha:  B)
-       (iota: A -> B):=
+       (alpha:  B) (iota: A -> B):=
   {
-  SubON_compare: forall x y : A,
+    SubON_compare: forall x y : A,
       compareB (iota x) (iota y) = compareA x y;
   SubON_incl : forall x, ltB (iota x) alpha;
   SubON_onto : forall y, ltB y alpha  -> exists x:A, iota x = y}.
@@ -104,11 +103,10 @@ Class  SubON
 Class  ON_Iso 
        `(OA : @ON A ltA compareA)
        `(OB : @ON B ltB compareB)
-       (f : A -> B)
-       (g : B -> A):=
+       (f : A -> B) (g : B -> A):=
   {
-  iso_compare :forall x y : A,  compareB (f x) (f y) =
-                                compareA x y;
+    iso_compare :forall x y : A,
+      compareB (f x) (f y) = compareA x y;
   iso_inv1 : forall a, g (f a)= a;
   iso_inv2 : forall b, f (g b) = b
   }.
diff --git a/theories/ordinals/OrdinalNotations/ON_Omega2.v b/theories/ordinals/OrdinalNotations/ON_Omega2.v
index 3a7ff0f7..e235fcaa 100644
--- a/theories/ordinals/OrdinalNotations/ON_Omega2.v
+++ b/theories/ordinals/OrdinalNotations/ON_Omega2.v
@@ -583,9 +583,10 @@ Section Merge.
     end.
   (* ... *)
 (* end snippet Merge *) 
-  
-  - intros; unfold m, measure_lt; cbn; destruct xs0; simpl; left; abstract lia.
-  - intros; unfold m, measure_lt; cbn; destruct ys0; simpl; right; abstract lia.
+  - intros; unfold m, measure_lt; cbn; destruct xs0 ;simpl;left;
+      abstract lia.
+  - intros; unfold m, measure_lt; cbn; destruct ys0; simpl; right;
+      abstract lia.
   - apply wf_measure. 
   Defined.
 
diff --git a/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v b/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v
index df22c30f..8b84d40d 100644
--- a/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v
+++ b/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v
@@ -14,10 +14,10 @@ Open Scope opo_scope.
 
 (* begin snippet OmegaPlusOmegaDef:: no-out *)
 
-#[ global] Instance compare_nat_nat : Compare t :=
+#[global] Instance compare_nat_nat : Compare t :=
  compare_t compare_nat compare_nat.
 
-#[ global] Instance Omega_plus_Omega: ON _ compare_nat_nat :=
+#[global] Instance Omega_plus_Omega: ON _ compare_nat_nat :=
  ON_plus Omega Omega.
 
 Definition t := ON_t.
@@ -398,7 +398,7 @@ Lemma Omega_as_lub  :
 
  (* begin snippet Incl *)
  
- #[ global ] Instance Incl : SubON Omega Omega_plus_Omega omega fin. (* .no-out *)
+ #[ global] Instance Incl : SubON Omega Omega_plus_Omega omega fin. (* .no-out *)
 
  (* end snippet Incl *)
  Proof.
diff --git a/theories/ordinals/OrdinalNotations/OmegaOmega.v b/theories/ordinals/OrdinalNotations/OmegaOmega.v
index cbf2aa32..df3a8af7 100644
--- a/theories/ordinals/OrdinalNotations/OmegaOmega.v
+++ b/theories/ordinals/OrdinalNotations/OmegaOmega.v
@@ -73,21 +73,21 @@ Module LO.
     | cons i n beta => limitb beta
     end.
 
-  Lemma succb_ref (a:t): succb a -> T1.succb (refine a).
+  Lemma succb_ref (a:t): succb a -> T1is_succ (refine a).
   Proof.
     induction a as [| a l]; cbn.
     - trivial.
     - destruct a as [n n0]; now destruct n.
   Qed.
 
-  Lemma limitb_ref (a:t): limitb a -> T1.limitb (refine a).
+  Lemma limitb_ref (a:t): limitb a -> T1limit (refine a).
   Proof.
     induction a as [| a l]; cbn.
     - trivial.
     -  destruct a as [n n0].
        destruct n.
        + discriminate.
-       + simpl T1.limitb; destruct l. 
+       + simpl T1limit; destruct l. 
          * trivial.
          * intro H; rewrite IHl; case (refine (p::l)); auto.
   Qed.
diff --git a/theories/ordinals/solutions_exercises/F_3.v b/theories/ordinals/solutions_exercises/F_3.v
index b597bf70..c1fcc1b7 100644
--- a/theories/ordinals/solutions_exercises/F_3.v
+++ b/theories/ordinals/solutions_exercises/F_3.v
@@ -150,7 +150,7 @@ Section S1.
 
       (* TODO: simplify this proof ! *)
       Lemma L04 : forall beta:T1,
-          limitb beta ->
+          T1limit beta ->
           forall n, leq lt  (\F (S n)) (Canon.canon beta (S n)).
       Proof.
         destruct beta.
diff --git a/theories/ordinals/solutions_exercises/Limit_Infinity.v b/theories/ordinals/solutions_exercises/Limit_Infinity.v
index 4a97670d..f198cb98 100644
--- a/theories/ordinals/solutions_exercises/Limit_Infinity.v
+++ b/theories/ordinals/solutions_exercises/Limit_Infinity.v
@@ -18,7 +18,7 @@ Section On_alpha.
   Hypothesis HnonZero : alpha <> zero.
 
   Section S1.
-    Hypothesis H : limitb  alpha.
+    Hypothesis H : T1limit  alpha.
 
     Variable beta : T1.
     Hypothesis Hbeta : beta t1< alpha.
@@ -73,7 +73,7 @@ Section On_alpha.
     Hypothesis H :  forall beta, beta t1< alpha ->
                                  exists gamma, beta t1< gamma t1< alpha.
 
-    Lemma L4 : limitb alpha.
+    Lemma L4 : T1limit alpha.
     Proof.
       destruct (zero_limit_succ_dec Halpha) as [[Hzero | Hlim] | Hsucc].
       - now destruct HnonZero.
@@ -91,7 +91,7 @@ Section On_alpha.
 
   End S2.
 
-  Theorem Limit_Infinity : limitb alpha <-> (forall beta,
+  Theorem Limit_Infinity : T1limit alpha <-> (forall beta,
                                                 beta t1< alpha -> Infinite (fun gamma =>  beta t1< gamma t1< alpha)).
   Proof.
     split; intro H.

From c32def5c08062a15672d27de96e2d363993c40e0 Mon Sep 17 00:00:00 2001
From: Pierre Casteran <pierre.casteran@labri.fr>
Date: Wed, 18 May 2022 16:13:03 +0200
Subject: [PATCH 02/11] revision book (chapter 4)

---
 doc/epsilon0-chapter.tex                      |  31 ++--
 theories/ordinals/Epsilon0/T1.v               |  70 ++++-----
 .../ordinals/OrdinalNotations/ON_Generic.v    |   6 +-
 .../ordinals/OrdinalNotations/OmegaOmega.v    | 140 +++++++++---------
 theories/ordinals/Prelude/Iterates.v          |   3 +-
 theories/ordinals/Prelude/MoreLibHyps.v       |   2 +-
 theories/ordinals/Schutte/Correctness_E0.v    |   8 +-
 7 files changed, 129 insertions(+), 131 deletions(-)

diff --git a/doc/epsilon0-chapter.tex b/doc/epsilon0-chapter.tex
index 1b0940de..3664a9b4 100644
--- a/doc/epsilon0-chapter.tex
+++ b/doc/epsilon0-chapter.tex
@@ -519,6 +519,7 @@ \subsubsection{Successor}
 \label{Functions:succ-T1}
 
 \vspace{4pt}
+\noindent
 \emph{From Module~\href{../theories/html/hydras.Epsilon0.T1.html\#succ}{Epsilon0.T1}}
 
 
@@ -531,8 +532,8 @@ \subsubsection{Successor}
 
 \input{movies/snippets/T1/succbIff}
 
-\begin{exercise}[\gaiasign]
-  Look for the \gaia-theorem which corresponds to \texttt{T1is\_succ\_iff}.
+\begin{exercise}
+  \gaiasign Look for the \gaia-theorem which corresponds to \texttt{T1is\_succ\_iff}.
 \end{exercise}
 
 \subsubsection{Successor function on \texttt{E0}}
@@ -736,25 +737,35 @@ \subsubsection{Using a stronger inductive predicate.}
 \inputsnippets{E0/E0LtWf}
 
 
-\begin{remark}
+\begin{remark}[Related work]
 \label{remark:a3pat}
-The alternate proof of well-foundedness using \'Evelyne Contejean's work on
-    recursive path ordering~\cite{DershowitzRPO, a3pat} is available in the
+A proof of well-foundedness using \'Evelyne Contejean's work on
+    recursive path ordering~\cite{DershowitzRPO, a3pat} is also available in the
     library \href{../theories/html/hydras.Epsilon0.Epsilon0rpo.html}{Epsilon0.Epsilon0rpo}.
+
+    In~\cite{Manolios2005}, Manolios and Vroom prove the well-foundedness of ordinal terms below $\epsilon_0$ by reduction to the natural order on the set of natural numbers.
  \end{remark}
 
 
 
 \subsection{An ordinal notation for  \texorpdfstring{$\epsilon_0$}{epsilon0}}
 
-We build an instance of \texttt{ON}, and prove its correctness w.r.t. Schutte's model (see Chapter~\ref{chap:schutte}).
 
+We are now able to build an instance of \texttt{ON}.
+
+\vspace{4pt}
+\noindent
 \emph{From Module~\href{../theories/html/hydras.Epsilon0.E0.html}{Epsilon0.E0}}
 
 \input{movies/snippets/E0/InstanceEpsilon0}
 
 \label{instance-epsilon0}
 
+
+We prove also that this notation is correct w.r.t. Schutte's model (see Chapter~\ref{chap:schutte}).
+
+\vspace{4pt}
+\noindent
 \emph{From Module~\href{../theories/html/hydras.Schutte.Correctness_E0.html}{Schutte.Correctness\_E0}}
 
 
@@ -799,7 +810,7 @@ \subsection{An ordinal notation for  \gaia's ordinals}
 
  
 
-    \section{A refinement of \texttt{E0} : an ordinal notation for \texorpdfstring{$\omega^\omega$}{omega\^omega}}
+    \section{An ordinal notation for \texorpdfstring{$\omega^\omega$}{omega\^omega}}
 
     In Module   \href{https://github.com/coq-community/hydra-battles/blob/master/theories/
       ordinals/OrdinalNotations/OmegaOmega.v}{theories/ordinals/OrdinalNotations/OmegaOmega.v},
@@ -850,7 +861,7 @@ \subsection{An ordinal notation for  \gaia's ordinals}
 
 
     
-\begin{exercise}[not trivial]
+\begin{exercise}
   It may be interesting to write a \emph{direct} proof  of well-foundedness of the order in $\omega^\omega$ (\emph{i.e.}
   without using properties of $\epsilon_0$). This exercise may
   help to understand better the proof structure of Sect.~\vref{sec:strongly-accessible}.
@@ -1043,7 +1054,7 @@ \subsection{An ordinal notation for  \gaia's ordinals}
 
     We prove  the commutativity of $\oplus$ in two steps. 
     First, we prove by transfinite induction on $\alpha$ that the restriction of $\oplus$ to the
-    interval $[0..\alpha)$ is commutative.
+    interval $[0,\alpha)$ is commutative.
 
     \index{maths}{Transfinite induction}
 
@@ -1139,7 +1150,7 @@ \subsection{An ordinal notation for  \gaia's ordinals}
     \end{itemize}
 
     So, a  natural question is `` Does there exist any strictly decreasing variant mapping
-    type \texttt{Hydra} into some interval $[0,\alpha)$ (where $\alpha <\epsilon_0$) for proving the termination of all hydra battles''. The next chapter is dedicated to a formal proof that there exists no such $\alpha$, even if we consider a restriction to the set of ``standard'' battles.
+    type \texttt{Hydra} into some interval $[0,\mu)$ (where $\mu <\epsilon_0$) for proving the termination of all hydra battles''. The next chapter is dedicated to a formal proof that there exists no such $\mu$, even if we consider a restriction to the set of ``standard'' battles.
 
 
 
diff --git a/theories/ordinals/Epsilon0/T1.v b/theories/ordinals/Epsilon0/T1.v
index 3d0105b1..472fd454 100644
--- a/theories/ordinals/Epsilon0/T1.v
+++ b/theories/ordinals/Epsilon0/T1.v
@@ -99,8 +99,7 @@ Fixpoint T1is_succ alpha :=
     | cons zero _ _ => true
     | cons alpha n beta => T1is_succ beta
   end.
-#[deprecated(note="use T1is_succ")]
- Notation succb := T1is_succ (only parsing).
+
 
 
 Fixpoint T1limit alpha :=
@@ -111,9 +110,6 @@ Fixpoint T1limit alpha :=
     | cons alpha n beta => T1limit beta
   end.
 
-#[deprecated(note="use T1limit")]
-  Notation limitb := T1limit (only parsing).
-
 Compute T1limit T1omega.
 
 Compute T1limit 42.
@@ -123,6 +119,11 @@ Compute T1is_succ 42.
 Compute T1is_succ T1omega.
 
 (* end snippet succbLimitb *)
+#[deprecated(note="use T1is_succ")]
+  Notation succb := T1is_succ (only parsing).
+
+#[deprecated(note="use T1limit")]
+  Notation limitb := T1limit (only parsing).
 
 (** Exponential of base [omega] *)
 
@@ -559,13 +560,12 @@ Definition epsilon_0 : Ensemble T1 := nf.
 (** *** Successor *)
 
 (* begin snippet succDef *)
-
-Fixpoint succ (alpha:T1) : T1 :=
-  match alpha with zero => T1nat 1
+Fixpoint succ (a: T1) : T1 :=
+  match a with
+  | zero => T1nat 1
   | cons zero n _ => cons zero (S n) zero
-  | cons beta n gamma => cons beta n (succ gamma)
+  | cons b n c => cons b n (succ c)
   end.
-
 (* end snippet succDef *)
 
 (** *** Predecessor (partial function *)
@@ -586,8 +586,8 @@ Fixpoint pred (c:T1) : option T1 :=
 (* begin snippet plusDef *)
 
 
-Fixpoint T1add (alpha beta : T1) :T1 :=
-  match alpha,beta with
+Fixpoint T1add (a b : T1) :T1 :=
+  match a, b with
   |  zero, y  => y
   |  x, zero  => x
   |  cons a n b, cons a' n' b' =>
@@ -603,13 +603,12 @@ where "alpha + beta" := (T1add alpha beta) : t1_scope.
 #[deprecated(note="use T1add")]
   Notation plus := T1add (only parsing).
 
-
 (** *** multiplication *)
 
 (* begin snippet multDef *)
 
-Fixpoint T1mul (alpha beta : T1) :T1 :=
-  match alpha,beta with
+Fixpoint T1mul (a b : T1) :T1 :=
+  match a, b with
   |  zero, _  => zero
   |  _, zero => zero
   |  cons zero n _, cons zero n' b' =>
@@ -619,7 +618,7 @@ Fixpoint T1mul (alpha beta : T1) :T1 :=
   |  cons a n b, cons a' n' b' =>
       cons (a + a') n' ((cons a n b) * b')
   end
-where "alpha * beta" := (T1mul alpha beta) : t1_scope.
+where "a * b" := (T1mul a b) : t1_scope.
 
 (* end snippet multDef *)
 #[deprecated(note="use T1mul")]
@@ -1598,9 +1597,8 @@ Module Direct_proof.
       Lemma wf_LT : forall alpha: T1,  nf alpha -> Acc LT alpha. 
       Proof.
         induction alpha as [| beta IHbeta n gamma IHgamma].
-        - split.
-          inversion 1.
-          destruct H2 as [H3 _]. destruct (not_lt_zero H3). 
+        - split. intros y H0; inversion H0 as [_ [H3 _]];
+            destruct (not_lt_zero H3). 
         (*||*)
         (*|
 .. coq:: -.h#beta -.h#n -.h#gamma -.h#H 
@@ -1863,9 +1861,9 @@ Qed.
 
 (* begin snippet succIsPlusOne:: no-out *)
 
-Lemma succ_is_plus_one (alpha : T1) :  succ alpha = alpha + 1.
+Lemma succ_is_plus_one (a : T1) :  succ a = a + 1.
 Proof. 
-  induction alpha as [ |a IHa n b IHb]; [trivial |]. 
+  induction a as [ |a IHa n b IHb]; [trivial |]. 
   (* ... *)
   (* end snippet succIsPlusOne *)
    - destruct  a; cbn.
@@ -1876,21 +1874,21 @@ Qed.
 (* end snippet succIsPlusOnez *)
 
 Lemma succ_of_plus_finite :
-  forall alpha (H: nf alpha) (i:nat) , succ (alpha + i) = alpha + S i.
+  forall a (H: nf a) (i:nat) , succ (a + i) = a + S i.
 Proof.
-  induction  alpha; cbn.
+  induction  a; cbn.
   -  destruct i; reflexivity.
   -  destruct i.
      + simpl.
-       destruct alpha1.
+       destruct a1.
        * simpl; replace (n + 0)%nat with n.
          { auto. }
          { abstract lia. }
        * simpl; rewrite succ_is_plus_one; auto.
-     + simpl; destruct alpha1.
+     + simpl; destruct a1.
        * simpl; replace (S (n + i)) with (n + S i)%nat; auto.
-       *  simpl; assert (nf alpha2) by eauto with T1.
-          generalize  (IHalpha2 H0 (S i)).
+       *  simpl; assert (nf a2) by eauto with T1.
+          generalize  (IHa2 H0 (S i)).
           replace (T1nat (S i)) with (FS i); auto.
           replace (T1nat (S (S  i))) with (FS (S i)).
           {intro H1; now rewrite H1. }
@@ -2112,19 +2110,13 @@ Qed.
 
 (* begin snippet notMono:: no-out  *)
 
-Lemma plus_not_monotonous_l :
-  exists alpha beta gamma : T1,
-    alpha t1< beta /\ alpha + gamma = beta + gamma.
-Proof.
-  exists 3, 5, T1omega; now compute.
-Qed.
+Lemma T1add_not_monotonous_l :
+  exists a b c : T1, a t1< b /\ a + c = b + c.
+Proof. exists 3, 5, T1omega; now compute. Qed.
 
-Lemma mult_not_monotonous :
-  exists alpha beta gamma : T1,
-      alpha t1< beta /\ alpha * gamma = beta * gamma.
-Proof.
-  exists 3, 5, T1omega; now compute.
-Qed.
+Lemma T1mul_not_monotonous :
+  exists a b c : T1, c <> zero /\ a t1< b /\ a * c = b * c.
+Proof. exists 3, 5, T1omega; split; [discriminate| now compute]. Qed.
 (* end snippet notMono *)
 
 
diff --git a/theories/ordinals/OrdinalNotations/ON_Generic.v b/theories/ordinals/OrdinalNotations/ON_Generic.v
index 62c09f0c..557e30cf 100644
--- a/theories/ordinals/OrdinalNotations/ON_Generic.v
+++ b/theories/ordinals/OrdinalNotations/ON_Generic.v
@@ -159,13 +159,11 @@ Definition SubON_same_fun `{OA : @ON A ltA  compareA}
 
 Definition SubON_same_op `{OA : @ON A ltA compareA}
        `{OB : @ON B ltB  compareB}
-       {iota : A -> B} 
-       {alpha: B}
+       {iota : A -> B} {alpha: B}
        {_ : SubON OA OB alpha iota}
        (f : A -> A -> A)
        (g : B -> B -> B)
-  :=
-  forall x y,  iota (f x y) = g (iota x) (iota y).
+  := forall x y,  iota (f x y) = g (iota x) (iota y).
 
 (* end snippet SubONSameOp *)
 
diff --git a/theories/ordinals/OrdinalNotations/OmegaOmega.v b/theories/ordinals/OrdinalNotations/OmegaOmega.v
index df3a8af7..fae82e88 100644
--- a/theories/ordinals/OrdinalNotations/OmegaOmega.v
+++ b/theories/ordinals/OrdinalNotations/OmegaOmega.v
@@ -3,9 +3,10 @@
 (** New implementation as a refinement of epsilon0 *)
 
 Require Import T1 E0.
-Require Import Arith  Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec  List Bool
-        Recdef Lia  Coq.Wellfounded.Inverse_Image
-        Coq.Wellfounded.Inclusion RelationClasses  Logic.Eqdep_dec.
+Require Import Arith  Coq.Logic.Eqdep_dec Coq.Arith.Peano_dec
+  List Bool
+  Recdef Lia  Coq.Wellfounded.Inverse_Image
+  Coq.Wellfounded.Inclusion RelationClasses  Logic.Eqdep_dec.
 
 
 Require Import Comparable.
@@ -17,7 +18,7 @@ Module LO.
   
   Definition t := list (nat*nat).
 
-  Definition zero : t := (@nil (nat * nat): t).
+  Definition zero : t := nil. 
 
   (** omega^ i * S n + alpha *)
 
@@ -34,11 +35,6 @@ Module LO.
 
   Notation phi0 i := (cons i 0 nil).
 
-  (** [omega ^i * (k+1)] *)
-  
-  Definition omega_term (i k: nat) : t :=
-    cons i k zero.
-
   Notation omega := (phi0 1). 
 
   (* end snippet LODef *)
@@ -58,19 +54,19 @@ Module LO.
 
   (** Successor and limits (syntactic definitions) *)
 
-  Fixpoint succb (alpha:t) :=
-    match alpha with
+  Fixpoint succb (a : t) :=
+    match a with
       nil => false
     | cons 0 _ _ => true
-    | cons i n beta => succb beta
+    | cons i n b => succb b
     end.
   
-  Fixpoint limitb (alpha:t) :=
-    match alpha with
+  Fixpoint limitb (a : t) :=
+    match a with
       nil => false
     | cons 0 _ _ => false
     | cons i n nil => true
-    | cons i n beta => limitb beta
+    | cons i n b => limitb b
     end.
 
   Lemma succb_ref (a:t): succb a -> T1is_succ (refine a).
@@ -94,8 +90,8 @@ Module LO.
 
   (* begin snippet compareDef:: no-out  *)
   #[ global ] Instance compare_t : Compare t :=
-  fix cmp (alpha beta:t) :=
-    match alpha, beta with
+  fix cmp (a b : t) :=
+    match a, b with
     | nil, nil => Eq
     | nil, cons a' n' b' => Datatypes.Lt
     | _   , nil => Gt
@@ -110,15 +106,15 @@ Module LO.
        end)
     end.
   
-  Lemma compare_ref (alpha beta:t) :
-    compare alpha beta = compare (refine alpha) (refine beta).
+  Lemma compare_ref (a b : t) :
+    compare a b = compare (refine a) (refine b).
  (* end snippet compareDef  *)  
   Proof.
-    revert beta. induction alpha.
-    - destruct beta.
+    revert b; induction a.
+    - destruct b.
       + easy.
       + cbn. now destruct p.
-    - destruct a, beta.
+    - destruct a, b.
       + now cbn.
       + destruct  p; cbn.
         destruct (n ?= n1) eqn: cn_n1;
@@ -127,19 +123,19 @@ Module LO.
   Qed.
 
   (* begin snippet ltDef *)
-  Definition lt (alpha beta : t) : Prop :=
-    compare alpha beta = Datatypes.Lt.
+  Definition lt (a b : t) : Prop :=
+    compare a b = Datatypes.Lt.
   (* end snippet ltDef *)
   
   Lemma compare_rev :
-    forall (alpha beta : t),
-      compare beta alpha = CompOpp (compare alpha beta).
+    forall (a b : t),
+      compare b a = CompOpp (compare a b).
   Proof.
-    induction alpha,  beta.
+    induction a, b.
     - easy.
     - cbn; destruct p; cbn; trivial. 
     - cbn; destruct a; reflexivity. 
-    - cbn; rewrite IHalpha. destruct p, a;  rewrite Nat.compare_antisym.
+    - cbn; rewrite IHa. destruct p, a;  rewrite Nat.compare_antisym.
       destruct (Nat.compare n1 n) eqn:? ; cbn; trivial.
       rewrite Nat.compare_antisym;
         destruct  (Nat.compare n2 n0) eqn:? ; now cbn.
@@ -148,29 +144,29 @@ Module LO.
   
 
   Lemma compare_reflect :
-    forall alpha beta,
-      match compare alpha beta with
-      | Datatypes.Lt => lt alpha beta
-      | Eq => alpha = beta
-      | Gt => lt beta alpha
+    forall a b,
+      match compare a b with
+      | Datatypes.Lt => lt a b
+      | Eq => a = b
+      | Gt => lt b a
       end.
   Proof.
-    unfold lt; induction alpha  as [ | [p n]].
-    - destruct beta.
+    unfold lt; induction a  as [ | [p n]].
+    - destruct b.
       + easy.
       + cbn; now destruct p.
-    - destruct beta as [ | [p0 n0] beta]. 
+    - destruct b as [ | [p0 n0] b]. 
       + cbn; trivial.
-      + cbn; specialize (IHalpha beta);
-          rewrite compare_rev with alpha beta; 
+      + cbn; specialize (IHa b);
+          rewrite compare_rev with a b;
           rewrite Nat.compare_antisym in * ;
-          destruct (compare alpha beta), (p0 ?= p) eqn:Heq; simpl in *;
+          destruct (compare a b), (p0 ?= p) eqn:Heq; simpl in *;
             subst; try easy;
               apply Nat.compare_eq_iff in Heq as -> ;
               destruct (n ?= n0) eqn:Heqc; trivial.
         * destruct (compare _ _) eqn: H.
           apply Nat.compare_eq_iff in Heqc as ->.
-          rewrite IHalpha.
+          rewrite IHa.
           reflexivity.
           reflexivity.
           rewrite Nat.compare_antisym.
@@ -180,7 +176,7 @@ Module LO.
             now rewrite Nat.compare_antisym, Heqn.
         * destruct (compare _ _) eqn: H.
           apply Nat.compare_eq_iff in Heqc as ->.
-          rewrite IHalpha.
+          rewrite IHa.
           reflexivity.
           reflexivity.
           rewrite Nat.compare_antisym.
@@ -190,7 +186,7 @@ Module LO.
           rewrite Nat.compare_antisym; now rewrite Heqc0.
         * destruct (compare _ _) eqn: H.
           apply Nat.compare_eq_iff in Heqc as ->.
-          rewrite IHalpha.
+          rewrite IHa.
           reflexivity.
           reflexivity.
           rewrite Nat.compare_antisym.
@@ -201,11 +197,11 @@ Module LO.
           reflexivity.
   Qed.
 
-  Lemma compare_correct (alpha beta: t):
-    CompSpec eq lt alpha beta (compare alpha beta).
+  Lemma compare_correct (a b: t):
+    CompSpec eq lt a b (compare a b).
   Proof.
-    unfold lt;  generalize (compare_reflect alpha beta).
-    destruct (compare alpha beta); now constructor.
+    unfold lt;  generalize (compare_reflect a b).
+    destruct (compare a b); now constructor.
   Qed.
 
   (* begin snippet ltRef:: no-out *)
@@ -233,14 +229,13 @@ Module LO.
          destruct (T1.lt_irrefl H).
   Qed.
 
-  Lemma lt_irrefl (alpha: t): ~ lt alpha alpha.
+  Lemma lt_irrefl (a : t): ~ lt a a.
   Proof.
     rewrite lt_ref; now apply T1.lt_irrefl.
   Qed.
 
 
-  Lemma lt_trans (alpha beta gamma : t):
-    lt alpha beta -> lt beta gamma -> lt alpha gamma.
+  Lemma lt_trans (a b c : t): lt a b -> lt b c -> lt a c.
   Proof.
     rewrite !lt_ref; apply T1.lt_trans.
   Qed.
@@ -268,8 +263,7 @@ Module LO.
       (nf_b b && Nat.ltb a' a)%bool
     end.
 
-  Definition nf alpha :Prop := 
-    nf_b alpha.
+  Definition nf alpha :Prop := nf_b alpha.
 (* end snippet nfDef *)
   (** refinements of T1's lemmas *)
 
@@ -281,7 +275,6 @@ Module LO.
     destruct i; red; now cbn.
   Qed. 
 
-
   Lemma single_nf :
     forall i n, nf (cons i n zero).
   Proof. unfold nf; now cbn. Qed. 
@@ -328,23 +321,23 @@ Module LO.
   Qed.
 
 
-  Lemma nf_ref: forall alpha, T1.nf (refine alpha) <-> nf alpha.
+  Lemma nf_ref: forall a, T1.nf (refine a) <-> nf a.
   Proof.
-    induction alpha.
+    induction a.
     - cbn; split; trivial.
     - destruct a as [i n];  split.
-      + intro H;  destruct alpha.
+      + intro H;  destruct a0.
         * apply single_nf.
         * destruct p.
           apply cons_nf.
           -- cbn in H; apply T1.nf_inv3 in H; now apply T1.lt_fin_iff. 
-          -- cbn in H; apply IHalpha; apply T1.nf_inv2 in H; apply H.
-      + intro H; destruct alpha.
+          -- cbn in H; apply IHa; apply T1.nf_inv2 in H; apply H.
+      + intro H; destruct a0.
         * apply T1.single_nf, T1.nf_fin.
         * destruct p; cbn; apply T1.cons_nf.
           --  apply nf_inv3 in H; now apply T1.lt_fin_iff.
           -- apply T1.nf_fin.
-          -- apply nf_inv2 in H; now rewrite IHalpha.
+          -- apply nf_inv2 in H; now rewrite IHa.
   Qed.
 
 
@@ -354,15 +347,15 @@ Module LO.
 
   (* begin snippet succPlusMult *)
   
-  Fixpoint succ (alpha : t) : t :=
-    match alpha with
-      nil => fin 1
+  Fixpoint succ (a : t) : t :=
+    match a with
+    | nil => fin 1
     | cons 0 n _  => cons 0 (S n) nil
-    | cons a n beta => cons a n (succ beta)
+    | cons a n b => cons a n (succ b)
     end.
 
-  Fixpoint plus (alpha beta : t) :t :=
-    match alpha,beta with
+  Fixpoint plus (a b : t) :t :=
+    match a, b with
     |  nil, y  => y
     |  x, nil  => x
     |  cons a n b, cons a' n' b' =>
@@ -372,10 +365,10 @@ Module LO.
         | Eq  => (cons a (S (n+n')) b')
         end)
     end
-  where "alpha + beta" := (plus alpha beta) : lo_scope.
+  where "a + b" := (plus a b) : lo_scope.
 
-  Fixpoint mult (alpha beta : t) : t :=
-    match alpha,beta with
+  Fixpoint mult (a b : t) : t :=
+    match a, b with
     |  nil, _  => zero
     |  _, nil => zero
     |  cons 0 n _, cons 0 n' b' =>
@@ -385,7 +378,7 @@ Module LO.
     |  cons a n b, cons a' n' b' =>
        cons (a + a')%nat n' ((cons a n b) * b')
     end
-  where "alpha * beta" := (mult alpha beta) : lo_scope.
+  where "a * b" := (mult a b) : lo_scope.
 
 
   Compute omega * omega.
@@ -422,7 +415,8 @@ Module LO.
 
   Lemma succ_nf alpha : nf alpha -> nf (succ alpha).
   Proof.
-    intro H; rewrite <- nf_ref in *; rewrite succ_ref; now apply T1.succ_nf.
+    intro H; rewrite <- nf_ref in *; rewrite succ_ref;
+      now apply T1.succ_nf.
   Qed.
 
   (* begin snippet plusRef:: no-out  *)
@@ -436,7 +430,8 @@ Module LO.
     - cbn; destruct a. now cbn.
     - destruct a, p; cbn;  destruct (n ?= n1) eqn:cn_n1.
       1,2:   rewrite T1.compare_fin_rw in *; rewrite cn_n1; now cbn.
-      rewrite T1.compare_fin_rw in *; cbn;rewrite cn_n1, IHalpha; now cbn.
+      rewrite T1.compare_fin_rw in *; cbn;rewrite cn_n1, IHalpha;
+        now cbn.
   Qed.
 
 
@@ -459,7 +454,8 @@ Module LO.
        + cbn; destruct p; now cbn.
     - induction beta.
       +  destruct a; cbn. destruct n; now cbn.
-      +  destruct a, a0; cbn. destruct n; cbn. destruct n1; cbn; trivial.
+      +  destruct a, a0; cbn. destruct n; cbn.
+         destruct n1; cbn; trivial.
          * f_equal; rewrite IHbeta; f_equal.
          * cbn. destruct n1. cbn. reflexivity.
            cbn. f_equal. f_equal. lia.
@@ -654,7 +650,7 @@ Import OO.
 
 Check phi0  7.
 
-#[local] Coercion Fin : nat >-> OO.
+#[global] Coercion Fin : nat >-> OO.
 
 Example Ex42: omega + 42 + omega^ 2 = omega^ 2. (* .no-out *)
 rewrite <- Comparable.compare_eq_iff.
diff --git a/theories/ordinals/Prelude/Iterates.v b/theories/ordinals/Prelude/Iterates.v
index 4ae7ce3d..f7e32dd4 100644
--- a/theories/ordinals/Prelude/Iterates.v
+++ b/theories/ordinals/Prelude/Iterates.v
@@ -10,7 +10,8 @@ Open Scope nat_scope.
 From Coq Require Import RelationClasses Relations Arith Max Lia.
 From hydras Require Import Exp2.
 
-From hydras Require Import MoreLibHyps.
+From LibHyps Require Import LibHyps.
+From hydras  Require Import MoreLibHyps.
 Ltac rename_hyp n th ::= rename_short n th.
 
 (* begin snippet iterateDef *)
diff --git a/theories/ordinals/Prelude/MoreLibHyps.v b/theories/ordinals/Prelude/MoreLibHyps.v
index 7027aa52..5a3a7668 100644
--- a/theories/ordinals/Prelude/MoreLibHyps.v
+++ b/theories/ordinals/Prelude/MoreLibHyps.v
@@ -1,4 +1,4 @@
-From LibHyps Require Export LibHyps.
+From LibHyps Require Import LibHyps.
 
 Require Import List.
 Import ListNotations. 
diff --git a/theories/ordinals/Schutte/Correctness_E0.v b/theories/ordinals/Schutte/Correctness_E0.v
index 53df6d23..282bece0 100644
--- a/theories/ordinals/Schutte/Correctness_E0.v
+++ b/theories/ordinals/Schutte/Correctness_E0.v
@@ -24,10 +24,10 @@ Import List  PartialFun Ensembles.
 (* begin snippet injectDef *)
 
 Fixpoint inject (t:T1) : Ord :=
- match t with T1.zero => zero
-         | T1.cons a n b =>
-           AP._phi0 (inject a) * S n + inject b
- end.
+  match t with
+  | T1.zero => zero
+  | T1.cons a n b => AP._phi0 (inject a) * S n + inject b
+  end.
 
 (* end snippet injectDef *)
 

From 4942c667d0291521e1d260659f495ea770611b16 Mon Sep 17 00:00:00 2001
From: Pierre Casteran <pierre.casteran@labri.fr>
Date: Thu, 19 May 2022 14:16:53 +0200
Subject: [PATCH 03/11] book re-reading

---
 doc/epsilon0-chapter.tex                      | 20 +++----
 doc/ks-chapter.tex                            | 57 ++++++++++---------
 doc/large-sets-chapter.tex                    |  6 +-
 theories/gaia/GCanon.v                        |  3 +-
 theories/ordinals/Epsilon0/Canon.v            | 26 ++++-----
 theories/ordinals/Epsilon0/Large_Sets.v       | 11 ++--
 theories/ordinals/Epsilon0/Paths.v            | 25 +++-----
 .../ordinals/Hydra/Epsilon0_Needed_Free.v     |  8 ++-
 .../ordinals/Hydra/Epsilon0_Needed_Generic.v  | 16 ++----
 theories/ordinals/Hydra/Epsilon0_Needed_Std.v |  5 +-
 theories/ordinals/Hydra/O2H.v                 | 42 ++++++--------
 11 files changed, 97 insertions(+), 122 deletions(-)

diff --git a/doc/epsilon0-chapter.tex b/doc/epsilon0-chapter.tex
index 3664a9b4..648dc1d9 100644
--- a/doc/epsilon0-chapter.tex
+++ b/doc/epsilon0-chapter.tex
@@ -1139,18 +1139,18 @@ \subsection{An ordinal notation for  \gaia's ordinals}
 
     \inputsnippets{GHydra/mDef, GHydra/mVariant, GHydra/Termination}
     
-    \section*{Conclusion}
+    % \section*{Conclusion}
 
-    Let us recall three results we have proved so far.
-    \begin{itemize}
-    \item There exists a strictly decreasing variant which maps \texttt{Hydra} into 
-    the segment $[0,\epsilon_0)$ for proving the termination of any hydra battle
-    \item There exists \emph{no} such variant from \texttt{Hydra} into 
-    $[0,\omega^2)$, \emph{a fortiori} into $[0,\omega)$.
-    \end{itemize}
+    % Let us recall three results we have proved so far.
+    % \begin{itemize}
+    % \item There exists a strictly decreasing variant which maps \texttt{Hydra} into 
+    % the segment $[0,\epsilon_0)$ for proving the termination of any hydra battle
+    % \item There exists \emph{no} such variant from \texttt{Hydra} into 
+    % $[0,\omega^2)$, \emph{a fortiori} into $[0,\omega)$.
+    % \end{itemize}
 
-    So, a  natural question is `` Does there exist any strictly decreasing variant mapping
-    type \texttt{Hydra} into some interval $[0,\mu)$ (where $\mu <\epsilon_0$) for proving the termination of all hydra battles''. The next chapter is dedicated to a formal proof that there exists no such $\mu$, even if we consider a restriction to the set of ``standard'' battles.
+    % So, a  natural question is `` Does there exist any strictly decreasing variant mapping
+    % type \texttt{Hydra} into some interval $[0,\mu)$ (where $\mu <\epsilon_0$) for proving the termination of all hydra battles''. The next chapter is dedicated to a formal proof that there exists no such $\mu$, even if we consider a restriction to the set of ``standard'' battles.
 
 
 
diff --git a/doc/ks-chapter.tex b/doc/ks-chapter.tex
index e419cd52..e5b40099 100644
--- a/doc/ks-chapter.tex
+++ b/doc/ks-chapter.tex
@@ -31,7 +31,7 @@ \section{Introduction}
 \end{quote}
 
 Our proofs are  constructive and require no axioms: they are  closed terms of the CIC, and are mainly composed on function definitions and proofs of properties of these functions. 
-They  share much theoretical material with Kirby and Paris', although they do not use any knowledge about Peano arithmetic nor model  theory.  The combinatorial arguments we use and implement
+They  borrow much theoretical material from Kirby and Paris, although they do not use any knowledge about Peano arithmetic nor model  theory.  The combinatorial arguments we use and implement
 come from 
  an article by J.~Ketonen and R.~Solovay~\cite{KS81}, already  cited in the work
  by L.~Kirby and J.~Paris. % on the termination of Goodstein sequences and hydra battles~\cite{KP82}.
@@ -49,31 +49,33 @@ \section{Canonical Sequences}
 
 \index{maths}{Transfinite induction}
 \begin{itemize}
-\item If $\alpha\not=0$, then $\canonseq{\alpha}{i}<\alpha$. Thus canonical sequences can be used for proofs by transfinite induction or function definition by transfinite recursion
+\item If $\alpha\not=0$, then $\canonseq{\alpha}{i}<\alpha$. Thus canonical sequences can be used in proofs by transfinite induction or function definition by transfinite recursion
 \item If $\lambda$ is a limit ordinal, then $\lambda$ is the least upper bound of the set 
 $\{\canonseq{\lambda}{i}\;|\,i\in\mathbb{N}_1\}$
 
 
 \item If $\beta<\alpha<\epsilon_0$, then there is a ``path'' from $\alpha$ to $\beta$, \emph{i.e.} a
 sequence $\alpha_0=\alpha, \alpha_1, \dots, \alpha_n=\beta$, where for every $k<n$, there exists some $i_k$ such that $\alpha_{k+1}=\canonseq{\alpha_k}{i_k}$
-\item Canonical sequences correspond tightly to rounds of hydra battles: if $\alpha\not=0$,
-then $\iota(\alpha)$ is transformed into $\iota(\canonseq{\alpha}{i+1})$ in one round with
-the replication factor $i$ (Lemma \href{../theories/html/hydras.Hydra.O2H.html\#canonS_iota_i}{Hydra.O2H.canonS\_iota\_i}).
-\item From the two previous properties, we infer that whenever $\beta<\alpha<\epsilon_0$, there exists a (free) battle from $\iota(\alpha)$ to $\iota(\beta)$.
 \end{itemize}
 
 \begin{remark}
-  In~\cite{KS81}, canonical sequences are defined for any ordinal $\alpha <\epsilon_0$,
+  Canonical sequences are defined for any ordinal $\alpha <\epsilon_0$,
 by stating that if $\alpha$ is a successor ordinal $\beta+1$,  the sequence associated with 
 $\alpha$ is simply the constant sequence whose terms are equal to $\beta$.
 Likewise, the canonical sequence of $0$ maps any natural number to $0$.
 
-This convention allows us to make total the function that maps any ordinal $\alpha$ and natural number $i$ to the ordinal $\canonseq{\alpha}{i}$.
-
+Thus, the function that maps any ordinal $\alpha$ and natural number $i$ to the ordinal $\canonseq{\alpha}{i}$ is total.
 \end{remark}
 
+\subsection{Canonical sequences and hydra battles}
 
-First, let us recall how canonical sequences are defined in~\cite{KS81}. For efficiency's sake, we decided not to implement directly K.\&S's definitions, but to define in \gallina{} simply typed structurally recursive functions which share the abstract properties which are used in the mathematical proofs\footnote{With a small difference: the $0$-th term of the canonical sequence is not the same in our development as in~\cite{KS81}.}.
+Canonical sequences correspond tightly to rounds of hydra battles: if $\alpha\not=0$,
+then $\iota(\alpha)$ is transformed into $\iota(\canonseq{\alpha}{i+1})$ in one round with
+the replication factor $i$ (Lemma \href{../theories/html/hydras.Hydra.O2H.html\#canonS_iota_i}{Hydra.O2H.canonS\_iota\_i}).
+Thus, whenever $\beta<\alpha<\epsilon_0$, there exists a (free) battle from $\iota(\alpha)$ to $\iota(\beta)$.
+
+\subsection{Definitions}
+First, let us recall how canonical sequences are defined in~\cite{KS81}. For efficiency's sake, we decided not to implement directly K.\&S's definitions, but to define in \gallina{} simply typed structurally recursive functions which share the abstract properties which are used in the mathematical proofs.
 
 
 
@@ -125,8 +127,10 @@ \subsubsection{Canonical sequences in \coq}
 
 \input{movies/snippets/Canon/canonDef}
 
-\paragraph*{\gaiasign} Our library~\href{../theories/html/gaia_hydras.GCanon.html}{gaia\_hydras.GCanon} transposes the  function \texttt{canon} into \gaia's type \texttt{T1}
-(please see Sect.\~ref{sect:gcanon}).
+\paragraph*{\gaiasign}
+The translation of \texttt{canon} compatible with \gaia's data-types is
+defined in ~\href{../theories/html/gaia_hydras.GCanon.html\#canon}{gaia\_hydras.GCanon} (please see Sect.~\ref{sect:gcanon}).
+
 \index{gaiabridge}{Canonical sequences}
 \paragraph*{Remark}
 In the present state of this library, the following specializations of \texttt{canon} are still used in some proofs or lemma statements. They are planned to be deprecated.
@@ -195,8 +199,7 @@ \subsubsection{Limit ordinals are truly limits}
 \label{lemma:canonS-limit}
 
 
-Note the use of \coq's \texttt{sig} type in the theorem's statement, which
-relates the boolean function \texttt{T1limit} defined on the \texttt{T1} data-type with a constructive view of the limit of a sequence: for any $\beta<\lambda$, we can compute an item of the canonical sequence of $\lambda$ which is greater than $\beta$.
+Note the use of \coq's \texttt{sig} type in the theorem's statement, which expresses a constructive view of the limit of a sequence: for any $\beta<\lambda$, we can compute an item of the canonical sequence of $\lambda$ which is greater than $\beta$.
 We can also state directly that $\lambda$ is a (strict) least upper bound of the elements of its canonical sequence.
 
 \input{movies/snippets/Canon/canonSLimitLub}
@@ -232,7 +235,8 @@ \section{Accessibility inside \texorpdfstring{$\epsilon_0$}{epsilon0}\,: paths}
 \label{sect:pathes-intro}
 
 Let us consider a kind of accessibility problem inside $\epsilon_0$: given two ordinals $\alpha$ and $\beta$, where $\beta<\alpha<\epsilon_0$, find a \emph{path} consisting of a finite sequence $\gamma_0=\alpha,\dots,\gamma_l=\beta$,
-where, for every $i<l$, $\gamma_i \not= 0$ \footnote{This condition allows us to ignore paths which end by a lot of useless $0$s.} and there exists some strictly positive integer $s_i$
+where, for every $i<l$, $\gamma_i \not= 0$
+and there exists some strictly positive integer $s_i$
 such that $\gamma_{i+1}=\canonseq{\gamma}{s_i}$.
 
 Let $s$ be the sequence $\langle s_0,s_1,\dots, s_{l-1} \rangle$. We describe the
@@ -247,15 +251,15 @@ \section{Accessibility inside \texorpdfstring{$\epsilon_0$}{epsilon0}\,: paths}
   
 
 Note that, given $\alpha$ and $\beta$, where $\beta < \alpha$, the sequence $s$ which leads from $\alpha$ to $\beta$ is not unique.
-Indeed, if $\alpha$ is a limit ordinal, the first element of $s$ can be any integer $i$ such that $\beta<\canonseq{\alpha}{i}$, and if $\alpha$ is a successor ordinal,
-then the sequence $s$ can start with any positive integer.
 
 
-For instance, we have also 
-$\omega*2 \xrightarrow[3,4,5,6]{}\omega$. 
+
+For instance, we have 
+$\omega\times 2 \xrightarrow[2]{}\omega$ and
+$\omega\times 2 \xrightarrow[3,4,5,6]{}\omega$. 
 Likewise,
-$\omega*2 \xrightarrow[1,2,1,4]{} 0$ and
-$\omega*2 \xrightarrow[3,3,3,3,3,3,3,3]{} 0$.
+$\omega\times 2 \xrightarrow[1,2,1,4]{} 0$ and
+$\omega\times 2 \xrightarrow[3,3,3,3,3,3,3,3]{} 0$.
 \end{remark}
 
 \subsection{Formal definition}
@@ -285,7 +289,7 @@ \subsection{Formal definition}
 \paragraph*{\gaiasign}
 
 The library~\href{../theories/html/gaia_hydras.GPaths.html}{gaia\_hydras.GPaths} transposes the  notion of path into \gaia's type \texttt{T1}
-(please see Sect.\~ref{sect:gpath}).
+(please see Sect.~\ref{sect:gpath}).
 
 
 \index{hydras}{Exercises}
@@ -312,7 +316,7 @@ \subsection{Existence of a path}
 
 
 \noindent 
-From the lemma \texttt{canon\_LT}~\vref{lemma:canon_LT}, we can convert any path into an inequality on ordinals (by induction on paths).
+By the lemma \texttt{canon\_LT}~(Sct.\vref{lemma:canon_LT}), we can convert any path into an inequality on ordinals (by induction on paths).
 
 \input{movies/snippets/Paths/pathToLT}
 
@@ -532,12 +536,13 @@ \section{The case of standard battles}
 
 
 
-Our goal is now  to transform any inequality $\beta<\alpha<\epsilon_0$ into a standard path $\alpha \xrightarrow[i,j]{} \beta$ for some $i$ and $j$, then into a standard battle
-from $\iota(\alpha+i)$ to $\iota(\beta)$. 
+Our goal is now  to transform any inequality $\beta<\alpha<\epsilon_0$ into a standard path $\alpha \xrightarrow[i,j]{} \beta$ for some $i$ and $j$, which corresponds to a standard battle
+from $\iota(\alpha)$ (at time $i$)  to $\iota(\beta)$
+(at time $j$) .
 Following~\cite{KS81}, we proceed in two stages:
 \begin{enumerate}
 \item we simulate plain (free) paths from $\alpha$ to $\beta$ with
-paths made of steps $(\gamma,\canonseq{\gamma}{n})$, \emph{with the same $n$ all along the path}
+paths made of steps $(\gamma,\canonseq{\gamma}{n})$, \emph{with the same $n$ all along the path}.
 \item we simulate any such path by a standard path.
 \end{enumerate}
 
diff --git a/doc/large-sets-chapter.tex b/doc/large-sets-chapter.tex
index a42d8d03..c3b5b7ea 100644
--- a/doc/large-sets-chapter.tex
+++ b/doc/large-sets-chapter.tex
@@ -1,7 +1,7 @@
 \chapter{Large sets and rapidly growing functions}\label{chap:alpha-large}
 
 \begin{remark}
-Some notations (mainly names of fast-growing functions) of our development may differ slightly from the literature. Although this fact does not affect our proofs, we are preparing a future version where the names $F\_alpha$, $f\_alpha$, $H\_alpha$, etc., are fully consistent with the cited articles.
+Some notations (mainly names of fast-growing functions) of our development may differ slightly from the literature. Although this fact does not affect our proofs, we are preparing a future version where the names $F_\alpha$, $f_\alpha$, $H_\alpha$, etc., are fully consistent with the cited articles.
 
 \end{remark}
 %\section{Introduction}
@@ -109,7 +109,7 @@ \subsection{Examples}
 \section{Length of minimal large sequences}
 \label{sect:lalpha-section}
 
-Now, consider any natural number $k>0$ any ordinal $0<\alpha<\epsilon_0$.  We would like to compute
+Now, let us consider some natural number $k>0$ and an ordinal $0<\alpha<\epsilon_0$.  We would like to compute
 a number $l$ such that the interval $[k,l]$ is $\alpha$-mlarge. So, 
 the standard battle starting with $\iota(\alpha)$ and the replication factor $k$ will end after $(l-k+1)$ steps.
 
@@ -136,7 +136,7 @@ \section{Length of minimal large sequences}
 use \coq{} to reason  about the \emph{specification} of \texttt{L},
 prove properties of any function which satisfies this specification.
 In Sect.~\ref{sect:L-equations}, we use the \texttt{coq-equations} plug-in
-to define a function \texttt{L\_}, and prove its correctness w.r.t. its specification.
+to define  \texttt{L\_}, then prove its correctness w.r.t. its specification.
 
 
 \subsection{Formal specification}
diff --git a/theories/gaia/GCanon.v b/theories/gaia/GCanon.v
index 6c04f5ce..3d77079e 100644
--- a/theories/gaia/GCanon.v
+++ b/theories/gaia/GCanon.v
@@ -92,8 +92,7 @@ Proof.
 Qed. 
 
 (* begin snippet gcanonLt:: no-out *)
-Lemma canon_lt  (i : nat) [a : T1]:
-   T1nf a -> a <> zero -> canon a i < a.
+Lemma canon_lt (i : nat) [a : T1]: T1nf a -> a <> zero -> canon a i < a.
 (* end snippet gcanonLt *)
 Proof. 
   case: i => [| n Hnf Hpos].  
diff --git a/theories/ordinals/Epsilon0/Canon.v b/theories/ordinals/Epsilon0/Canon.v
index fc7ee7a8..2b15308b 100644
--- a/theories/ordinals/Epsilon0/Canon.v
+++ b/theories/ordinals/Epsilon0/Canon.v
@@ -26,17 +26,17 @@ Open Scope t1_scope.
 (* begin snippet canonDef *)
 Fixpoint canon alpha (i:nat) : T1 :=
   match alpha with
-    zero => zero
+  | zero => zero
   | cons zero 0 zero  => zero
   | cons zero (S k) zero  => FS k
   | cons gamma 0 zero => (match T1.pred gamma with
                             Some gamma' =>
-                            match i with 0 => zero
-                                    |   S j => cons gamma' j zero
-                            end
-                          | None =>
-                            cons (canon gamma i) 0 zero
-                           end)
+                              match i with
+                              | 0 => zero
+                              | S j => cons gamma' j zero
+                              end
+                          | None => cons (canon gamma i) 0 zero
+                          end)
   
   |  cons gamma (S n) zero =>
      (match T1.pred gamma with
@@ -86,11 +86,9 @@ End Canon_examples.
 
 (* begin snippet canonS0 *)
 
-Definition  canonS alpha (i:nat) : T1 :=
-  canon alpha (S i).
+Definition  canonS alpha (i:nat) : T1 := canon alpha (S i).
 
-Definition  canon0 alpha  : T1 :=
-  canon alpha 0.
+Definition  canon0 alpha  : T1 := canon alpha 0.
 
 (* end snippet canonS0 *)
 
@@ -665,10 +663,8 @@ limit of its  own canonical sequence
 
 (*| .. coq:: no-out *)
 Lemma canonS_limit_strong lambda : 
-  nf lambda ->
-  T1limit lambda  ->
-  forall beta, beta t1< lambda ->
-               {i:nat | beta t1< canon lambda (S i)}.
+  nf lambda -> T1limit lambda  ->
+  forall beta, beta t1< lambda -> {i:nat | beta t1< canon lambda (S i)}.
 Proof.
   transfinite_induction lambda.
   (* ... *) (*||*) (*| .. coq:: none |*)
diff --git a/theories/ordinals/Epsilon0/Large_Sets.v b/theories/ordinals/Epsilon0/Large_Sets.v
index 354d412e..db2bcdef 100644
--- a/theories/ordinals/Epsilon0/Large_Sets.v
+++ b/theories/ordinals/Epsilon0/Large_Sets.v
@@ -452,9 +452,8 @@ Qed.
 (* begin snippet LOmegaOk:: no-out *)
 Lemma L_omega_ok : L_spec T1omega L_omega.
 Proof.
-  specialize
-    (L_lim_ok T1omega nf_omega refl_equal L_fin
-              (fun i => L_fin_ok (S i))); intro H.
+  pose (H:= L_lim_ok T1omega nf_omega refl_equal L_fin
+              (fun i => L_fin_ok (S i))).  
    eapply L_spec_compat with (1:=H); 
    intro ; unfold L_lim, L_fin, L_omega; abstract lia.
 Qed.
@@ -531,13 +530,12 @@ Qed.
 
 
 (* begin snippet LOmegaMultOk *)
-
 Lemma L_omega_mult_ok (i: nat) :
   L_spec (T1omega * i) (L_omega_mult i). (* .no-out *)
 (*| .. coq:: none |*)
 Proof.
  destruct i.
- - left;  intro k. reflexivity. 
+ - left; intro k; reflexivity. 
  - right.
    + cbn; discriminate.
    + intros k; unfold L_omega_mult, L_omega;
@@ -551,8 +549,7 @@ Qed.
 
 Lemma L_omega_mult_eqn (i : nat) :
   forall (k : nat),
-    (0 < k)%nat  ->
-    L_omega_mult i k = (exp2 i * S k - 1)%nat. (* .no-out *)
+    (0 < k)%nat  -> L_omega_mult i k = (exp2 i * S k - 1)%nat. (* .no-out *)
 (*| .. coq:: none |*)
 Proof.
   induction i.
diff --git a/theories/ordinals/Epsilon0/Paths.v b/theories/ordinals/Epsilon0/Paths.v
index ab191f9b..fdce4706 100644
--- a/theories/ordinals/Epsilon0/Paths.v
+++ b/theories/ordinals/Epsilon0/Paths.v
@@ -57,15 +57,11 @@ associated with   the [canonS i] functions. In module [O2H] we show how pathes a
 (* begin snippet pathDef *)
 
 Inductive path_to (beta: T1) : list nat -> T1 -> Prop :=
-  path_to_1 : forall (i:nat) alpha , 
-    i <> 0 ->
-    transition i alpha beta ->
-    path_to beta (i::nil) alpha
+| path_to_1 : forall (i:nat) alpha , 
+    i <> 0 -> transition i alpha beta -> path_to beta (i::nil) alpha
 | path_to_cons : forall i alpha s gamma,
-    i <> 0 ->
-    transition i alpha gamma ->
-    path_to beta  s gamma ->
-    path_to beta  (i::s) alpha.
+    i <> 0 -> transition i alpha gamma ->
+    path_to beta  s gamma -> path_to beta  (i::s) alpha.
 
 Definition path alpha s beta := path_to beta s alpha.
 
@@ -206,9 +202,8 @@ Definition standard_pathS  i alpha j beta :=
 
 (* begin snippet standardPathR *)
 
-Inductive standard_path_to (j:nat)(beta : T1)
-  : nat -> T1 -> Prop :=
-  std_1 : forall i alpha,
+Inductive standard_path_to (j:nat)(beta : T1): nat -> T1 -> Prop :=
+| std_1 : forall i alpha,
     alpha <> zero ->
     beta = canon alpha i -> j = i -> i <> 0 ->
     standard_path_to j beta i  alpha
@@ -1273,11 +1268,9 @@ Qed.
 
 (*| .. coq:: no-out |*)
 Theorem KS_thm_2_4 (lambda : T1) :
-   nf lambda ->
-   T1limit lambda  ->
-   forall i j, (i < j)%nat ->
-               const_path 1 (canon lambda (S j))
-                             (canon lambda (S i)).
+  nf lambda -> T1limit lambda  ->
+  forall i j, (i < j)%nat ->
+              const_path 1 (canon lambda (S j)) (canon lambda (S i)).
 Proof.
   transfinite_induction lambda.
   (* ... *)
diff --git a/theories/ordinals/Hydra/Epsilon0_Needed_Free.v b/theories/ordinals/Hydra/Epsilon0_Needed_Free.v
index 868af3ce..7352b4c7 100644
--- a/theories/ordinals/Hydra/Epsilon0_Needed_Free.v
+++ b/theories/ordinals/Hydra/Epsilon0_Needed_Free.v
@@ -36,13 +36,15 @@ Section Impossibility_Proof.
   
   Lemma m_ge : m big_h t1<= m small_h.
   Proof.
-    apply m_ge_generic with (1 := Hy). 
-    intros i h h' H; generalize Var; destruct 1.
+    apply m_ge_generic with (1 := Hy).
+    (* ... *)
+  (* end snippet mGe *)
+   intros i h h' H; generalize Var; destruct 1.
     apply variant_decr with i. 
     intro H0; subst; now apply (head_no_round_n _  _ H).
     exists i; apply H.      
   Qed.
-  (* end snippet mGe *)
+ 
   
   (** ** Proof of the inequality m small_h t1< m big_h 
    *)
diff --git a/theories/ordinals/Hydra/Epsilon0_Needed_Generic.v b/theories/ordinals/Hydra/Epsilon0_Needed_Generic.v
index e54a08d1..efec2eab 100644
--- a/theories/ordinals/Hydra/Epsilon0_Needed_Generic.v
+++ b/theories/ordinals/Hydra/Epsilon0_Needed_Generic.v
@@ -21,14 +21,11 @@ Section Bounded.
           (Var : Hvariant  T1_wf B m)
           (Hy : BoundedVariant  Var mu).
 
-  Hypothesis m_decrease : forall  i h h',
-      round_n i h h'-> m h' t1< m h.
+  Hypothesis m_decrease : forall  i h h', round_n i h h'-> m h' t1< m h.
   (* end snippet theContext *)
   
   Lemma  nf_m : forall h, nf (m h).
-  Proof.
-    intro h0; now destruct (m_bounded h0).
-  Qed.
+  Proof. intro h0; now destruct (m_bounded h0). Qed.
 
   Local Hint Resolve Rem0 : hydra.
   
@@ -38,7 +35,6 @@ Section Bounded.
   Lemma mu_positive : mu <> T1.zero.
   Proof. 
     intro H; subst;  specialize (m_bounded (hyd1 head)).
-    
     intro H0;  destruct (not_LT_zero H0). 
   Qed.
 
@@ -92,14 +88,10 @@ Section Bounded.
  Definition small_h := iota beta_h.
 
  Lemma mu_beta_h : acc_from mu beta_h.
- Proof.
-   apply LT_acc_from,  m_bounded. 
- Qed.
+ Proof. apply LT_acc_from, m_bounded.  Qed.
  
  Corollary m_ge_generic : m big_h t1<= m small_h.
- Proof.      
-   apply m_ge_0, nf_m.
- Qed.
+ Proof. apply m_ge_0, nf_m. Qed.
 
 End Bounded.
 (* end snippet mGeGeneric *)
diff --git a/theories/ordinals/Hydra/Epsilon0_Needed_Std.v b/theories/ordinals/Hydra/Epsilon0_Needed_Std.v
index 981898d6..974fefd5 100644
--- a/theories/ordinals/Hydra/Epsilon0_Needed_Std.v
+++ b/theories/ordinals/Hydra/Epsilon0_Needed_Std.v
@@ -212,12 +212,9 @@ Section Impossibility_Proof.
   
   Fact self_lt_standard : m big_h t1< m big_h.
   Proof. 
-    apply LE_LT_trans with (m small_h).
-    - apply m_ge. 
-    - apply m_lt.
+    apply LE_LT_trans with (m small_h);[apply m_ge | apply m_lt].
   Qed. 
 
-
   Theorem Impossibility_std: False.
   Proof.  apply (LT_irrefl self_lt_standard).  Qed.
 
diff --git a/theories/ordinals/Hydra/O2H.v b/theories/ordinals/Hydra/O2H.v
index f3433855..42940a11 100644
--- a/theories/ordinals/Hydra/O2H.v
+++ b/theories/ordinals/Hydra/O2H.v
@@ -18,19 +18,16 @@ Import Hydra_Definitions.
 
 (* begin snippet iotaDef *)
 
-Fixpoint iota (alpha : T1) : Hydra :=
-  match alpha with
+Fixpoint iota (a : T1) : Hydra :=
+  match a with
   | zero => head
-  | cons gamma n beta => node (hcons_mult (iota gamma) (S n)
-                                           (iotas beta))
+  | cons c n b => node (hcons_mult (iota c) (S n) (iotas b))
   end 
-with
-iotas (alpha : T1) :  Hydrae :=
-  match alpha with
-  | zero => hnil
-  | cons alpha0 n beta  => hcons_mult (iota alpha0) (S n)
-                                       (iotas beta)
-  end.
+with iotas (a : T1) :  Hydrae :=
+       match a with
+       | zero => hnil
+       | cons a0 n b  => hcons_mult (iota a0) (S n) (iotas b)
+       end.
 (* end snippet iotaDef *)
 
 (**  We now prove  a lot of technical lemmas that relate Hydras and 
@@ -532,15 +529,14 @@ Qed.
 
 (* begin snippet canonSIota *)
 
-Lemma canonS_iota i alpha :
-    nf alpha -> alpha <> 0 ->
-    iota alpha -1-> iota (canon alpha (S i)). (* .no-out *)
+Lemma canonS_iota i a :
+  nf a -> a <> 0 -> iota a -1-> iota (canon a (S i)). (* .no-out *)
 (*| .. coq:: none |*)
-  Proof.
-    intros;  destruct (canonS_iota_i i alpha  H H0).
-    - exists 0; now left.
-    - exists i; now right.
-  Qed.
+Proof.
+  intros;  destruct (canonS_iota_i i a  H H0).
+  - exists 0; now left.
+  - exists i; now right.
+Qed.
   (*||*)
   (* end snippet canonSIota *)
   
@@ -631,9 +627,8 @@ Qed.
 
   (* begin snippet pathToRoundPlus *)
   
-  Lemma path_to_round_plus alpha s beta :
-    path_to beta s alpha -> nf alpha ->
-    iota alpha -+-> iota beta. (* .no-out *)
+  Lemma path_to_round_plus a s b :
+    path_to b s a -> nf a -> iota a -+-> iota b. (* .no-out *)
   (*| .. coq:: none |*)
   Proof.
     intros H H0; apply path_to_path_toS in H.
@@ -657,8 +652,7 @@ Qed.
 
   (* begin snippet LTToRoundPlus *)
   
-  Lemma LT_to_round_plus alpha beta :
-    beta t1< alpha ->  iota alpha -+-> iota beta. (* .no-out *)
+  Lemma LT_to_round_plus a b : b t1< a ->  iota a -+-> iota b. (* .no-out *)
   (*| .. coq:: none |*)
   Proof.
     intros H; apply acc_from_to_round_plus; eauto with T1.

From 6777770a5e033cb5e0bc49b75afd95237c93f212 Mon Sep 17 00:00:00 2001
From: Karl Palmskog <palmskog@gmail.com>
Date: Thu, 19 May 2022 15:06:25 +0200
Subject: [PATCH 04/11] switch to general Coq Docker images for testing with
 Coq master due to MathComp Docker problems

---
 .github/workflows/docker-action.yml | 2 +-
 meta.yml                            | 3 +--
 2 files changed, 2 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml
index bba4e648..622c66e0 100644
--- a/.github/workflows/docker-action.yml
+++ b/.github/workflows/docker-action.yml
@@ -15,7 +15,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'coqorg/coq:dev-ocaml-4.13.1-flambda'
           - 'mathcomp/mathcomp:1.14.0-coq-8.15'
           - 'mathcomp/mathcomp:1.13.0-coq-8.14'
           - 'mathcomp/mathcomp:1.13.0-coq-8.13'
diff --git a/meta.yml b/meta.yml
index c514c93d..2e1d7fbf 100644
--- a/meta.yml
+++ b/meta.yml
@@ -107,8 +107,7 @@ supported_coq_versions:
   opam: '{(>= "8.13" & < "8.16~") | (= "dev")}'
 
 tested_coq_opam_versions:
-- version: 'coq-dev'
-  repo: 'mathcomp/mathcomp-dev'
+- version: 'dev-ocaml-4.13.1-flambda'
 - version: '1.14.0-coq-8.15'
   repo: 'mathcomp/mathcomp'
 - version: '1.13.0-coq-8.14'

From 08a39ef8285af5679b404d0ad17076bf8277742b Mon Sep 17 00:00:00 2001
From: Pierre Casteran <pierre.casteran@labri.fr>
Date: Thu, 19 May 2022 15:25:46 +0200
Subject: [PATCH 05/11] small changes description

---
 v09changes.md | 6 ++++++
 1 file changed, 6 insertions(+)
 create mode 100644 v09changes.md

diff --git a/v09changes.md b/v09changes.md
new file mode 100644
index 00000000..3951554d
--- /dev/null
+++ b/v09changes.md
@@ -0,0 +1,6 @@
+The experimental bridge to the [Gaia project](https://github.com/coq-community/gaia) allows now to import some definitions and theorems of the Ketonen-Solovay combinatorial theorems into the Gaia environment (see Chapter 7 of [the documentation](https://coq-community.org/hydra-battles/doc/hydras.pdf)).
+
+The first topics treated in this version are: canonical sequences, accessibility, and a few rapidly growing hierarchies of arithmetical functions.
+
+
+

From f4f8faf0c151ad81009b5f21c9fe8becf7fa7bba Mon Sep 17 00:00:00 2001
From: Pierre Casteran <pierre.casteran@labri.fr>
Date: Thu, 19 May 2022 15:32:44 +0200
Subject: [PATCH 06/11] small changes description

---
 v09changes.md | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/v09changes.md b/v09changes.md
index 3951554d..89dee530 100644
--- a/v09changes.md
+++ b/v09changes.md
@@ -1,4 +1,4 @@
-The experimental bridge to the [Gaia project](https://github.com/coq-community/gaia) allows now to import some definitions and theorems of the Ketonen-Solovay combinatorial theorems into the Gaia environment (see Chapter 7 of [the documentation](https://coq-community.org/hydra-battles/doc/hydras.pdf)).
+The experimental bridge to the [Gaia project](https://github.com/coq-community/gaia) allows now to import some definitions and theorems of the so-called Ketonen-Solovay combinatorial machinery into the Gaia environment (see Chapter 7 of [the documentation](https://coq-community.org/hydra-battles/doc/hydras.pdf)).
 
 The first topics treated in this version are: canonical sequences, accessibility, and a few rapidly growing hierarchies of arithmetical functions.
 

From 7debfee43385144269afcbf7fcaa97084994cc16 Mon Sep 17 00:00:00 2001
From: Pierre Casteran <pierre.casteran@labri.fr>
Date: Thu, 19 May 2022 19:16:51 +0200
Subject: [PATCH 07/11] fix deprecate warnings aout div2 and max

---
 theories/ordinals/Prelude/Fuel.v        | 2 +-
 theories/ordinals/Prelude/MoreVectors.v | 5 +++--
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/theories/ordinals/Prelude/Fuel.v b/theories/ordinals/Prelude/Fuel.v
index d250dbb0..a3791574 100644
--- a/theories/ordinals/Prelude/Fuel.v
+++ b/theories/ordinals/Prelude/Fuel.v
@@ -1,8 +1,8 @@
 
 (* Robert Krebbers's trick  *)
 
-Require Import Div2.
 Require Import FunInd Recdef Wf_nat Lia.
+Import Nat.
 
 Function zero (n:nat)  {wf lt n} : nat :=
   match n with
diff --git a/theories/ordinals/Prelude/MoreVectors.v b/theories/ordinals/Prelude/MoreVectors.v
index 1add9c72..16bd54c8 100644
--- a/theories/ordinals/Prelude/MoreVectors.v
+++ b/theories/ordinals/Prelude/MoreVectors.v
@@ -1,5 +1,6 @@
-Require Export Bool Arith Vector Max Lia.
-Import VectorNotations.
+Require Export Bool Arith Vector Lia.
+Import PeanoNat.Nat. 
+Import Vector VectorNotations.
 
 (** generalities on vectors *)
 

From 4ba7402da0ee25a959b280168bd12aaf7c34fe07 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre=20Cast=C3=A9ran?=
 <40755850+Casteran@users.noreply.github.com>
Date: Thu, 19 May 2022 21:23:15 +0200
Subject: [PATCH 08/11] Update doc/epsilon0-chapter.tex

Co-authored-by: Karl Palmskog <palmskog@gmail.com>
---
 doc/epsilon0-chapter.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/epsilon0-chapter.tex b/doc/epsilon0-chapter.tex
index 648dc1d9..a7fd3cdf 100644
--- a/doc/epsilon0-chapter.tex
+++ b/doc/epsilon0-chapter.tex
@@ -470,7 +470,7 @@ \subsubsection{\texttt{E0}: a sigma-type for \texorpdfstring{$\epsilon_0$}{epsil
 
 \paragraph*{\gaiasign}
 \index{gaiabridge}{Type of well formed ordinal terms below $\epsilon_0$}
- Our library~\href{../theories/html/gaia_hydras.T1Bridge.html}{gaia\_hydras.T1Bridge} defines also a type \texttt{E0} (which doesn't exist in \gaia-\texttt{ssete9}). 
+ Our library~\href{../theories/html/gaia_hydras.T1Bridge.html}{gaia\_hydras.T1Bridge} also defines a type \texttt{E0} (which doesn't exist in \gaia-\texttt{ssete9}). 
 
 
 

From 4cb9ca1507c0bbcacc4b775b3ebacb02b39c767f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre=20Cast=C3=A9ran?=
 <40755850+Casteran@users.noreply.github.com>
Date: Thu, 19 May 2022 21:23:36 +0200
Subject: [PATCH 09/11] Update doc/ks-chapter.tex

Co-authored-by: Karl Palmskog <palmskog@gmail.com>
---
 doc/ks-chapter.tex | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/doc/ks-chapter.tex b/doc/ks-chapter.tex
index e5b40099..3d9871b8 100644
--- a/doc/ks-chapter.tex
+++ b/doc/ks-chapter.tex
@@ -31,7 +31,7 @@ \section{Introduction}
 \end{quote}
 
 Our proofs are  constructive and require no axioms: they are  closed terms of the CIC, and are mainly composed on function definitions and proofs of properties of these functions. 
-They  borrow much theoretical material from Kirby and Paris, although they do not use any knowledge about Peano arithmetic nor model  theory.  The combinatorial arguments we use and implement
+They  borrow much theoretical material from Kirby and Paris, although they do not use any knowledge about Peano arithmetic nor about model  theory.  The combinatorial arguments we use and implement
 come from 
  an article by J.~Ketonen and R.~Solovay~\cite{KS81}, already  cited in the work
  by L.~Kirby and J.~Paris. % on the termination of Goodstein sequences and hydra battles~\cite{KP82}.

From 1bd63d03f866d2d782f6710fd3a5cbe43b6b7b1e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Pierre=20Cast=C3=A9ran?=
 <40755850+Casteran@users.noreply.github.com>
Date: Thu, 19 May 2022 21:24:12 +0200
Subject: [PATCH 10/11] Update
 theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v

Co-authored-by: Karl Palmskog <palmskog@gmail.com>
---
 theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v b/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v
index 8b84d40d..7fdb29a3 100644
--- a/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v
+++ b/theories/ordinals/OrdinalNotations/ON_Omega_plus_omega.v
@@ -398,7 +398,7 @@ Lemma Omega_as_lub  :
 
  (* begin snippet Incl *)
  
- #[ global] Instance Incl : SubON Omega Omega_plus_Omega omega fin. (* .no-out *)
+ #[global] Instance Incl : SubON Omega Omega_plus_Omega omega fin. (* .no-out *)
 
  (* end snippet Incl *)
  Proof.

From 4da0923ccd1908ae5e2cc922ad5d8f95802704db Mon Sep 17 00:00:00 2001
From: Pierre Casteran <pierre.casteran@labri.fr>
Date: Thu, 19 May 2022 22:19:07 +0200
Subject: [PATCH 11/11] new syntax for local and global directives

---
 theories/additions/Dichotomy.v                |  2 +-
 theories/additions/Euclidean_Chains.v         | 10 +++---
 theories/additions/FirstSteps.v               |  4 +--
 theories/additions/Monoid_def.v               |  4 +--
 theories/additions/Monoid_instances.v         | 14 ++++----
 theories/additions/More_on_positive.v         |  8 ++---
 theories/additions/Naive.v                    |  2 +-
 theories/additions/Pow.v                      |  6 ++--
 theories/additions/Pow_variant.v              |  4 +--
 theories/ordinals/Ackermann/misc.v            |  2 +-
 theories/ordinals/Epsilon0/Canon.v            |  3 +-
 theories/ordinals/Epsilon0/E0.v               |  9 ++---
 theories/ordinals/Epsilon0/Epsilon0rpo.v      | 18 +++++-----
 theories/ordinals/Epsilon0/F_alpha.v          |  4 +--
 theories/ordinals/Epsilon0/Hprime.v           |  4 +--
 theories/ordinals/Epsilon0/L_alpha.v          |  4 +--
 .../ordinals/Epsilon0/Large_Sets_Examples.v   |  2 +-
 theories/ordinals/Epsilon0/T1.v               | 24 ++++++-------
 theories/ordinals/Gamma0/Gamma0.v             | 34 +++++++++----------
 theories/ordinals/Gamma0/T2.v                 |  4 +--
 .../ordinals/Hydra/Epsilon0_Needed_Generic.v  |  2 +-
 theories/ordinals/Hydra/Hydra_Termination.v   |  2 +-
 theories/ordinals/Hydra/Omega_Small.v         |  2 +-
 .../ordinals/OrdinalNotations/ON_Generic.v    |  4 +--
 theories/ordinals/OrdinalNotations/ON_Omega.v |  5 ++-
 .../ordinals/OrdinalNotations/ON_Omega2.v     |  6 ++--
 theories/ordinals/OrdinalNotations/ON_plus.v  |  4 +--
 theories/ordinals/Prelude/Comparable.v        |  2 +-
 .../ordinals/Prelude/DecPreOrder_Instances.v  |  6 ++--
 theories/ordinals/Prelude/Fuel.v              |  7 ++--
 .../ordinals/Prelude/LibHyps_Experiments.v    |  2 +-
 theories/ordinals/Prelude/MoreLists.v         |  2 +-
 theories/ordinals/Prelude/MoreVectors.v       | 10 +++---
 theories/ordinals/Prelude/Sort_spec.v         |  4 +--
 theories/ordinals/Schutte/AP.v                |  4 +--
 theories/ordinals/Schutte/CNF.v               |  4 +--
 .../ordinals/Schutte/Ordering_Functions.v     | 18 +++++-----
 theories/ordinals/Schutte/Schutte_basics.v    | 28 +++++++--------
 theories/ordinals/Schutte/Well_Orders.v       |  4 +--
 theories/ordinals/rpo/list_permut.v           |  4 +--
 40 files changed, 141 insertions(+), 141 deletions(-)

diff --git a/theories/additions/Dichotomy.v b/theories/additions/Dichotomy.v
index 2cf61952..52b7c548 100644
--- a/theories/additions/Dichotomy.v
+++ b/theories/additions/Dichotomy.v
@@ -128,7 +128,7 @@ Proof.
     discriminate.
 Qed.
 
-Global Hint Resolve dicho_aux_le_xOXO dicho_aux_le_xOXI 
+#[global] Hint Resolve dicho_aux_le_xOXO dicho_aux_le_xOXI 
              dicho_aux_le_xIXO dicho_aux_le_xIXI : chains.
 
 Lemma dicho_aux_lt : forall p, 3 < p ->
diff --git a/theories/additions/Euclidean_Chains.v b/theories/additions/Euclidean_Chains.v
index 4d8fe6ae..60718c4e 100644
--- a/theories/additions/Euclidean_Chains.v
+++ b/theories/additions/Euclidean_Chains.v
@@ -489,7 +489,7 @@ $2^k.3^p$, using Fcompose and previous lemmas.
 Let us look at a simple example *)
 
 (* begin snippet F144 *)
-Global Hint Resolve F1_correct F1_proper
+#[global] Hint Resolve F1_correct F1_proper
      F3_correct F3_proper Fcompose_correct Fcompose_proper
      Fexp2_correct Fexp2_proper : chains.
 
@@ -858,7 +858,7 @@ Lemma KFK_proper : Kchain_proper (KFK kbr fq).
          * rewrite H2, H3;reflexivity. 
 Qed.
 
-Global Instance KFF_proper : Fchain_proper (KFF kbr fq).
+#[global] Instance KFF_proper : Fchain_proper (KFF kbr fq).
  Proof.
    intros until M; intros k k' Hk Hk' H x y Hxy;
    unfold KFF;   simpl.
@@ -1042,7 +1042,7 @@ Proof.
 Qed.
 
 (* begin snippet HintKchains *)
-Global Hint Resolve KFF_correct KFF_proper KFK_correct KFK_proper : chains.
+#[global] Hint Resolve KFF_correct KFF_proper KFK_correct KFK_proper : chains.
 (* end snippet HintKchains *)
 
 Lemma k3_1_correct : Kchain_correct 3 1 k3_1.
@@ -1059,7 +1059,7 @@ Proof.
   add_op_proper M H3; rewrite H2; reflexivity.
 Qed.
 
-Global Hint Resolve k3_1_correct k3_1_proper : chains.
+#[global] Hint Resolve k3_1_correct k3_1_proper : chains.
 
 (** an example of correct chain construction  *)
 
@@ -1185,7 +1185,7 @@ Definition  OK (s: signature)
 
 (* end snippet dependentlyTypedFuns *)
 
-Global Hint Resolve pos_gt_3 : chains.
+#[global] Hint Resolve pos_gt_3 : chains.
 
 (* begin snippet GammaContext *)
 Section Gamma.
diff --git a/theories/additions/FirstSteps.v b/theories/additions/FirstSteps.v
index fcea398c..cc62ed77 100644
--- a/theories/additions/FirstSteps.v
+++ b/theories/additions/FirstSteps.v
@@ -14,8 +14,8 @@ Section Definitions.
            (mult : A -> A -> A)
            (one : A).
 
-Local Infix "*" := mult.
-Local Notation "1" := one.
+#[local] Infix "*" := mult.
+#[local] Notation "1" := one.
 
 (**  Naive (linear) implementation *)
 
diff --git a/theories/additions/Monoid_def.v b/theories/additions/Monoid_def.v
index 27fda752..4ce00382 100644
--- a/theories/additions/Monoid_def.v
+++ b/theories/additions/Monoid_def.v
@@ -178,9 +178,9 @@ Every instance of class  [Monoid] can be transformed into an instance of
 *)
 
 (* begin snippet Coerciona:: no-out  *)
-Global Instance eq_equiv {A} : Equiv A := eq.
+#[global] Instance eq_equiv {A} : Equiv A := eq.
 
-Global Instance Monoid_EMonoid `(M:@Monoid A op one) :
+#[global] Instance Monoid_EMonoid `(M:@Monoid A op one) :
         EMonoid  op one eq_equiv.
 Proof.
 split; unfold eq_equiv, equiv in *.
diff --git a/theories/additions/Monoid_instances.v b/theories/additions/Monoid_instances.v
index d7df3fac..faca16b2 100644
--- a/theories/additions/Monoid_instances.v
+++ b/theories/additions/Monoid_instances.v
@@ -194,9 +194,9 @@ Qed.
 
 (* begin snippet M2Defsb:: no-out *)
 
-Global Instance M2_op : Mult_op M2 := M2_mult.
+#[global] Instance M2_op : Mult_op M2 := M2_mult.
 
-Global Instance M2_Monoid : Monoid   M2_op Id2.
+#[global] Instance M2_Monoid : Monoid   M2_op Id2.
 (* ... *)
 (* end snippet M2Defsb *)
 Proof. 
@@ -236,7 +236,7 @@ Section Nmodulo.
     intro H;subst m. discriminate. 
   Qed.
   
-  Local Hint Resolve m_neq_0 : chains.
+  #[local] Hint Resolve m_neq_0 : chains.
   
   (* begin snippet Nmodulob:: no-out *)
   Definition mult_mod (x y : N) := (x * y) mod m.
@@ -256,7 +256,7 @@ Section Nmodulo.
   Qed.
   
   (* begin snippet Nmoduloc:: no-out *)
-  Global Instance mult_mod_proper :
+  #[global] Instance mult_mod_proper :
     Proper (mod_equiv ==> mod_equiv ==> mod_equiv) mod_op.
   (* end snippet Nmoduloc *)
   Proof.
@@ -269,7 +269,7 @@ Section Nmodulo.
   Qed.
 
   (* begin snippet Nmodulod:: no-out *)
-  Local  Open Scope M_scope.
+  #[local]  Open Scope M_scope.
 
   Lemma mult_mod_associative :  forall x y z,
       x * (y * z) = x * y * z.
@@ -299,7 +299,7 @@ Section Nmodulo.
   
 
   (* begin snippet Nmodulog:: no-out *)  
-  Global Instance Nmod_Monoid : EMonoid  mod_op 1 mod_equiv.
+  #[global] Instance Nmod_Monoid : EMonoid  mod_op 1 mod_equiv.
   (* end snippet Nmodulog *)
   Proof.
     unfold equiv, mod_equiv, mod_eq, mult_op, mod_op, mult_mod.
@@ -318,7 +318,7 @@ Section S256.
 
   Let mod256 :=  mod_op 256.
 
-  Local Existing Instance mod256 | 1.
+  #[local] Existing Instance mod256 | 1.
 
   Compute (211 * 67)%M.
 
diff --git a/theories/additions/More_on_positive.v b/theories/additions/More_on_positive.v
index 9beb81dc..979f9204 100644
--- a/theories/additions/More_on_positive.v
+++ b/theories/additions/More_on_positive.v
@@ -23,7 +23,7 @@ Proof.
   discriminate.
 Qed.
 
-Global Hint Resolve Pos_to_nat_neq_0 : chains.
+#[global] Hint Resolve Pos_to_nat_neq_0 : chains.
 
 
 (** ** Relationship with [nat] and [N] 
@@ -34,7 +34,7 @@ Proof. discriminate. Qed.
 Lemma Npos_gt_0 : forall p, (0 < N.pos p)%N.
 Proof. reflexivity. Qed.
 
-Global Hint Resolve Npos_diff_zero  Npos_gt_0 : chains.
+#[global] Hint Resolve Npos_diff_zero  Npos_gt_0 : chains.
 
 
 Lemma pos2N_inj_lt : forall n p, (n < p)%positive <-> (N.pos n < N.pos p)%N.
@@ -87,7 +87,7 @@ Proof.
  apply Pos2Nat.inj_le; apply pos_le_mul.
 Qed.
 
-Global Hint Resolve Pos2Nat_le_1_p : chains.
+#[global] Hint Resolve Pos2Nat_le_1_p : chains.
 
 (** ** Surjection from [N] into [positive] 
 *)
@@ -239,7 +239,7 @@ Proof.
  -  split; intros; now compute.
 Qed.
 
-Global Hint Resolve pos_gt_3 : chains.
+#[global] Hint Resolve pos_gt_3 : chains.
 
 (** ** Lemmas on Euclidean division 
     N.pos_div_eucl (a:positive) (b:N) : N * N 
diff --git a/theories/additions/Naive.v b/theories/additions/Naive.v
index 97cd0c71..40dd1110 100644
--- a/theories/additions/Naive.v
+++ b/theories/additions/Naive.v
@@ -64,7 +64,7 @@ is still of type [nat].
 *)
 
 Module N_mod.
-Local Open Scope N_scope.
+#[local] Open Scope N_scope.
 
 Section m_fixed.
 
diff --git a/theories/additions/Pow.v b/theories/additions/Pow.v
index 36ea6c3a..da5be085 100644
--- a/theories/additions/Pow.v
+++ b/theories/additions/Pow.v
@@ -140,7 +140,7 @@ Section M_given.
           (M:EMonoid  E_op E_one E_eq).
 (* end snippet MGiven *)
 
-Global Instance Eop_proper : Proper (equiv ==> equiv ==> equiv) E_op.
+#[global] Instance Eop_proper : Proper (equiv ==> equiv ==> equiv) E_op.
 Proof.
   apply  Eop_proper.
 Qed.
@@ -157,7 +157,7 @@ Ltac monoid_simpl := repeat monoid_rw.
 (* *** Properties of the classical exponentiation  *)
 
 (* begin snippet powerProper:: no-out *)
-Global Instance power_proper :
+#[global] Instance power_proper :
   Proper (equiv ==> eq ==> equiv) power.
 (* end snippet powerProper *)
 Proof.
@@ -284,7 +284,7 @@ Proof.
     now monoid_rw.
 Qed.
 
-Global Instance Pos_bpow_proper :
+#[global] Instance Pos_bpow_proper :
   Proper  (equiv ==> eq ==> equiv) Pos_bpow.
 Proof.
   intros x y Hxy n p Hnp. subst n. revert  x y Hxy.
diff --git a/theories/additions/Pow_variant.v b/theories/additions/Pow_variant.v
index c2eb012a..21618389 100644
--- a/theories/additions/Pow_variant.v
+++ b/theories/additions/Pow_variant.v
@@ -127,7 +127,7 @@ Section M_given.
  Context (M:EMonoid  E_op E_one E_eq).
 
 
-Global Instance Eop_proper : Proper (equiv ==> equiv ==> equiv) E_op.
+#[global] Instance Eop_proper : Proper (equiv ==> equiv ==> equiv) E_op.
 apply  Eop_proper.
 Qed.
 
@@ -143,7 +143,7 @@ Ltac monoid_simpl := repeat monoid_rw.
 
 Section About_power.
 
-Global Instance power_proper : Proper (equiv ==> eq ==> equiv) power.
+#[global] Instance power_proper : Proper (equiv ==> eq ==> equiv) power.
 Proof.
   intros x y Hxy n p Hnp;  subst p; induction n.
   - reflexivity.
diff --git a/theories/ordinals/Ackermann/misc.v b/theories/ordinals/Ackermann/misc.v
index 596be162..5a03c829 100644
--- a/theories/ordinals/Ackermann/misc.v
+++ b/theories/ordinals/Ackermann/misc.v
@@ -1,6 +1,6 @@
 Require Import Eqdep_dec.
 
-Global Set Asymmetric Patterns.
+#[global] Set Asymmetric Patterns.
 
 Lemma inj_right_pair2 :
  forall A : Set,
diff --git a/theories/ordinals/Epsilon0/Canon.v b/theories/ordinals/Epsilon0/Canon.v
index 2b15308b..c1fb987b 100644
--- a/theories/ordinals/Epsilon0/Canon.v
+++ b/theories/ordinals/Epsilon0/Canon.v
@@ -1104,7 +1104,8 @@ Proof.
   simpl;   apply T1limit_canonS_not_zero; auto.
 Qed.
 
-Global Hint Resolve CanonS_lt Canon_lt Canon_of_limit_not_null : E0.
+#[global]
+  Hint Resolve CanonS_lt Canon_lt Canon_of_limit_not_null : E0.
 
 Lemma CanonS_phi0_Succ alpha i : CanonS (E0phi0 (E0succ alpha)) i =
                                  Omega_term alpha i.
diff --git a/theories/ordinals/Epsilon0/E0.v b/theories/ordinals/Epsilon0/E0.v
index 0f941bd1..11a309f2 100644
--- a/theories/ordinals/Epsilon0/E0.v
+++ b/theories/ordinals/Epsilon0/E0.v
@@ -345,7 +345,7 @@ Proof.
 Defined.
 (* end snippet E0LtWf *)
 
-Global Hint Resolve E0lt_wf : E0.
+#[global] Hint Resolve E0lt_wf : E0.
 
 Lemma Lt_Succ_Le (alpha beta: E0):  beta o< alpha -> E0succ beta o<= alpha.
 Proof.
@@ -397,14 +397,14 @@ Proof.
     apply LT_succ;auto.
 Qed.
 
-Global Hint Resolve E0pred_Lt : E0.
+#[global] Hint Resolve E0pred_Lt : E0.
 
 
 Lemma Succ_Succb (alpha : E0) : E0is_succ (E0succ alpha).
 destruct alpha; unfold E0is_succ, E0succ; cbn; apply T1.succ_is_succ.
 Qed.
 
-Global Hint Resolve Succ_Succb : E0.
+#[global] Hint Resolve Succ_Succb : E0.
 
 Ltac ord_eq alpha beta := assert (alpha = beta);
       [apply E0_eq_intro ; try reflexivity|].
@@ -451,7 +451,8 @@ Proof.
   intros H H0. rewrite (succ_not_limit _ H) in H0. discriminate.  
 Qed.
 
-Global Hint Resolve Limit_not_Zero Succ_not_Zero Lt_Succ Succ_not_T1limit : E0.
+#[global]
+  Hint Resolve Limit_not_Zero Succ_not_Zero Lt_Succ Succ_not_T1limit : E0.
 
 Lemma lt_Succ_inv : forall alpha beta, beta o< alpha <->
                                        E0succ beta o<= alpha.
diff --git a/theories/ordinals/Epsilon0/Epsilon0rpo.v b/theories/ordinals/Epsilon0/Epsilon0rpo.v
index 22f83c55..a484470e 100644
--- a/theories/ordinals/Epsilon0/Epsilon0rpo.v
+++ b/theories/ordinals/Epsilon0/Epsilon0rpo.v
@@ -173,7 +173,7 @@ Proof.
  simpl; auto with arith.
 Qed.
 
-Global Hint Resolve T1_size2 T1_size3 : rpo.
+#[global] Hint Resolve T1_size2 T1_size3 : rpo.
 
 
 (** let us recall subterm properties on T1 *)
@@ -198,9 +198,9 @@ Proof.
 Qed.
 
 
-Global Hint Resolve nat_lt_cons : rpo.
-Global Hint Resolve lt_subterm2 lt_subterm1 : rpo.
-Global Hint Resolve T1_size3 T1_size2 T1_size1 : rpo.
+#[global] Hint Resolve nat_lt_cons : rpo.
+#[global] Hint Resolve lt_subterm2 lt_subterm1 : rpo.
+#[global] Hint Resolve T1_size3 T1_size2 T1_size1 : rpo.
 
 
 Lemma nat_2_term_mono : forall n n', (n < n')%nat -> 
@@ -404,14 +404,14 @@ Remark R1 : Acc P.prec nat_0.
   destruct y; try contradiction.
 Qed.
 
-Global Hint Resolve R1 : rpo.
+#[global] Hint Resolve R1 : rpo.
 
 Remark R2 : Acc P.prec ord_zero. 
   split.
   destruct y; try contradiction; auto with rpo.
 Qed.
 
-Global Hint Resolve R2 : rpo.
+#[global] Hint Resolve R2 : rpo.
 
 Remark R3 : Acc P.prec nat_S.
   split.
@@ -419,14 +419,14 @@ Remark R3 : Acc P.prec nat_S.
 Qed.
 
 
-Global Hint Resolve R3 : rpo.
+#[global] Hint Resolve R3 : rpo.
 
 Remark R4 : Acc P.prec ord_cons.
   split.
   destruct y; try contradiction;auto with rpo.
 Qed.
 
-Global Hint Resolve R4 : rpo.
+#[global] Hint Resolve R4 : rpo.
 
 Theorem well_founded_rpo : well_founded rpo.
 Proof.
@@ -439,7 +439,7 @@ Section  well_founded.
   
   Let R := restrict  nf lt.
 
-  Local Hint Unfold restrict R : rpo.
+  #[local] Hint Unfold restrict R : rpo.
 
   Lemma R_inc_rpo : forall o o', R o o' -> rpo (T1_2_term o) (T1_2_term o').
   Proof.
diff --git a/theories/ordinals/Epsilon0/F_alpha.v b/theories/ordinals/Epsilon0/F_alpha.v
index f149983c..f3442b93 100644
--- a/theories/ordinals/Epsilon0/F_alpha.v
+++ b/theories/ordinals/Epsilon0/F_alpha.v
@@ -278,7 +278,7 @@ Section Properties.
       rewrite F_zero_eqn. rewrite LF1; abstract lia.
     Qed.
 
-    Local Hint Resolve F_One_Zero_dom mono_F_Zero Lt_n_F_Zero_n : T1.
+    #[local] Hint Resolve F_One_Zero_dom mono_F_Zero Lt_n_F_Zero_n : T1.
 
     Lemma F_One_Zero_ge :  F_ E0zero <<= F_ 1.
     Proof.
@@ -286,7 +286,7 @@ Section Properties.
         rewrite F_zero_eqn, LF1; abstract lia.  
     Qed. 
 
-    Local Hint Resolve  F_One_Zero_ge : T1.
+    #[local] Hint Resolve  F_One_Zero_ge : T1.
 
     Lemma PZero : P E0zero.
     Proof. 
diff --git a/theories/ordinals/Epsilon0/Hprime.v b/theories/ordinals/Epsilon0/Hprime.v
index 28160611..7d6db6e3 100644
--- a/theories/ordinals/Epsilon0/Hprime.v
+++ b/theories/ordinals/Epsilon0/Hprime.v
@@ -599,7 +599,7 @@ Section Proof_of_Abstract_Properties.
       - apply Succ_Succb.
     Qed.
 
-    Local Hint Resolve PD_Zero PA_Zero : E0.
+    #[local] Hint Resolve PD_Zero PA_Zero : E0.
 
     Lemma PC_Zero :  H'_ E0zero <<= H'_ (E0succ E0zero).
     Proof.
@@ -608,7 +608,7 @@ Section Proof_of_Abstract_Properties.
       rewrite E0pred_of_Succ, H'_eq1; auto with arith.
     Qed. 
 
-    Local Hint Resolve  PC_Zero : core.
+    #[local] Hint Resolve  PC_Zero : core.
 
     Lemma PZero : P E0zero.
     Proof. 
diff --git a/theories/ordinals/Epsilon0/L_alpha.v b/theories/ordinals/Epsilon0/L_alpha.v
index e7271ba9..c2e99703 100644
--- a/theories/ordinals/Epsilon0/L_alpha.v
+++ b/theories/ordinals/Epsilon0/L_alpha.v
@@ -13,8 +13,8 @@ From Coq Require Import ArithRing Lia.
 From Equations Require Import Equations.
 Import RelationClasses Relations.
 
-#[ global ] Instance Olt : WellFounded E0lt := E0lt_wf.
-Global Hint Resolve Olt : E0.
+#[global] Instance Olt : WellFounded E0lt := E0lt_wf.
+#[global] Hint Resolve Olt : E0.
 
 (** Using Coq-Equations for building a function which satisfies 
     [Large_sets.L_spec] *)
diff --git a/theories/ordinals/Epsilon0/Large_Sets_Examples.v b/theories/ordinals/Epsilon0/Large_Sets_Examples.v
index 28a6424b..db46f8fa 100644
--- a/theories/ordinals/Epsilon0/Large_Sets_Examples.v
+++ b/theories/ordinals/Epsilon0/Large_Sets_Examples.v
@@ -56,7 +56,7 @@ Compute  (gnaw (T1omega * T1omega) (interval 6 699)).
 
 Compute pp (  gnaw (T1omega * T1omega) (interval 6 509)).
 
-Global Hint Resolve iota_from_lt_not_In: core.
+#[global] Hint Resolve iota_from_lt_not_In: core.
 
 (* begin snippet Ex1Lemma:: no-out *)
 Example Ex1 : mlarge (T1omega * T1omega) (interval 6 510).
diff --git a/theories/ordinals/Epsilon0/T1.v b/theories/ordinals/Epsilon0/T1.v
index 472fd454..f176cafd 100644
--- a/theories/ordinals/Epsilon0/T1.v
+++ b/theories/ordinals/Epsilon0/T1.v
@@ -290,7 +290,7 @@ Qed.
 Theorem not_lt_zero alpha : ~ lt alpha  zero.
 Proof.  destruct alpha; compute; discriminate. Qed.
 
-Global Hint Resolve not_lt_zero : T1.
+#[global] Hint Resolve not_lt_zero : T1.
 
 Lemma compare_lt_impl a b :
   compare a b = Lt -> lt a b.
@@ -690,7 +690,7 @@ Qed.
 Lemma zero_lt : forall alpha n beta, lt zero (cons alpha n beta).
 Proof. reflexivity. Qed. 
 
-Global Hint Resolve zero_lt head_lt coeff_lt tail_lt : T1.
+#[global] Hint Resolve zero_lt head_lt coeff_lt tail_lt : T1.
 
 Open Scope t1_scope.
 
@@ -721,7 +721,7 @@ Proof.
     destruct b'2; intro H; now rewrite H.
 Qed.
 
-Global Hint Resolve zero_nf single_nf cons_nf: T1.
+#[global] Hint Resolve zero_nf single_nf cons_nf: T1.
 
 
 Lemma nf_inv1 :
@@ -834,7 +834,7 @@ Inductive nf_helper : T1 -> T1 -> Prop :=
                   nf_helper (cons alpha' n' beta') alpha.
 
 
-Global Hint Constructors nf_helper : T1.
+#[global] Hint Constructors nf_helper : T1.
 
 
 (* A tactic for decomposing a non zero ordinal *)
@@ -1032,7 +1032,7 @@ Proof.
 Qed.
 
 
-Global Hint Resolve zero_le le_tail : T1.
+#[global] Hint Resolve zero_le le_tail : T1.
 
 Theorem le_phi0 :
   forall a n b, leq lt  (phi0 a) (cons a n b).
@@ -1319,7 +1319,7 @@ Proof. now  destruct 1. Qed.
 Lemma LE_le alpha beta : alpha t1<= beta -> leq lt  alpha beta.
 Proof. now destruct 1. Qed.
 
-Global Hint Resolve LT_nf_r LT_nf_l LT_lt LE_nf_r LE_nf_l LE_le : T1.
+#[global] Hint Resolve LT_nf_r LT_nf_l LT_lt LE_nf_r LE_nf_l LE_le : T1.
 
 Lemma not_zero_lt : forall alpha, nf alpha -> alpha <> zero -> zero t1< alpha.
 Proof.
@@ -1394,7 +1394,7 @@ Lemma LT4 : forall alpha  n  beta beta',
     cons alpha n beta t1< cons alpha n beta'.
 Proof.   repeat split; auto; apply tail_lt.  destruct H1; tauto. Qed.
 
-Global Hint Resolve LT1 LT2 LT3 LT4: T1.
+#[global] Hint Resolve LT1 LT2 LT3 LT4: T1.
 
 
 Lemma LT_irrefl (alpha : T1) :
@@ -1443,9 +1443,9 @@ Proof.
   intros; apply cons_nf; auto; destruct H;tauto.
 Qed.
 
-Global Hint Resolve nf_cons_LT: T1.
+#[global] Hint Resolve nf_cons_LT: T1.
 
-Global Hint Resolve nf_inv1 nf_inv2 nf_inv3 : T1.
+#[global] Hint Resolve nf_inv1 nf_inv2 nf_inv3 : T1.
 
 Lemma head_LT_cons :
   forall alpha n beta,
@@ -1578,7 +1578,7 @@ Qed.
 
 Module Direct_proof.
   Section well_foundedness_proof.
-    Local Hint Unfold restrict LT: T1.
+    #[local] Hint Unfold restrict LT: T1.
 
     Lemma Acc_zero : Acc LT  zero.
     Proof.
@@ -2745,7 +2745,7 @@ Proof. compute; auto with T1. Qed.
 
 
 
-Global Hint Resolve nf_phi0 : T1.
+#[global] Hint Resolve nf_phi0 : T1.
 
 Definition omega_omega := phi0 T1omega.
 
@@ -3568,7 +3568,7 @@ Proof.
 Qed.
 
 
-Global Hint Resolve T1limit_not_zero : T1.
+#[global] Hint Resolve T1limit_not_zero : T1.
 
 
 Lemma T1limit_succ_tail :
diff --git a/theories/ordinals/Gamma0/Gamma0.v b/theories/ordinals/Gamma0/Gamma0.v
index e63d283e..4ab140ea 100644
--- a/theories/ordinals/Gamma0/Gamma0.v
+++ b/theories/ordinals/Gamma0/Gamma0.v
@@ -36,7 +36,7 @@ Proof.
   inversion_clear 1;auto with T2.
 Qed.
 
-Global Hint Resolve nf_a nf_b nf_c : T2.
+#[global] Hint Resolve nf_a nf_b nf_c : T2.
 
 Ltac nf_inv := ((eapply nf_a; eassumption)|| 
                 (eapply nf_b; eassumption)|| 
@@ -93,7 +93,7 @@ Proof.
   case gamma;auto with arith T2.
 Qed.
 
-Global Hint Resolve psi_le_cons le_zero_alpha: T2.
+#[global] Hint Resolve psi_le_cons le_zero_alpha: T2.
 
 Lemma le_psi_term_le alpha beta:  alpha t2<= beta ->
                                           psi_term alpha t2<= psi_term beta.
@@ -209,7 +209,7 @@ Section lemmas_on_length.
 
 End lemmas_on_length.
 
-Global Hint Resolve tricho_lt_7 tricho_lt_5 tricho_lt_4 tricho_lt_4' tricho_lt_3 tricho_lt_2 tricho_lt_2 : T2.
+#[global] Hint Resolve tricho_lt_7 tricho_lt_5 tricho_lt_4 tricho_lt_4' tricho_lt_3 tricho_lt_2 tricho_lt_2 : T2.
 
 Open Scope T2_scope.
 
@@ -643,7 +643,7 @@ Proof.
   - eapply psi_le_cons.
 Qed.
 
-Global Hint Resolve lt_beta_cons lt_alpha_cons : T2.
+#[global] Hint Resolve lt_beta_cons lt_alpha_cons : T2.
 
 Lemma le_cons_tail alpha beta n gamma gamma':
   gamma t2<= gamma' -> 
@@ -690,7 +690,7 @@ Proof.
   case a; case b; auto with T2.
 Qed.
 
-Global Hint Resolve le_one_cons : T2.
+#[global] Hint Resolve le_one_cons : T2.
 
 Lemma fin_lt_omega : forall n, fin  n t2<  omega.
 Proof.
@@ -834,7 +834,7 @@ Arguments compare_Lt [alpha beta].
 Arguments compare_Eq [alpha beta].
 
 
-Global Hint Resolve compare_Eq compare_Lt compare_Gt : T2.
+#[global] Hint Resolve compare_Eq compare_Lt compare_Gt : T2.
 
 Lemma compare_rw_lt  alpha beta : alpha t2< beta ->
                                   compare alpha beta = Lt.
@@ -1204,7 +1204,7 @@ Qed.
 
 
 
-Global Hint Resolve T2_size1 T2_size2 T2_size3 T2_size4 : T2.
+#[global] Hint Resolve T2_size1 T2_size2 T2_size3 T2_size4 : T2.
 
 
 (** let us recall subterm properties on T2 *)
@@ -1216,7 +1216,7 @@ Proof.
   intros; apply lt_trans with (gcons a b' n' c');auto with T2 .
 Qed.
 
-Global Hint Resolve nat_lt_cons lt_subterm1 : T2.
+#[global] Hint Resolve nat_lt_cons lt_subterm1 : T2.
 
 
 Lemma nat_2_term_mono : forall n n', (n < n')%nat -> 
@@ -1607,7 +1607,7 @@ Section lt_incl_rpo.
   Remark nf_b2 : nf b2.
   Proof. nf_inv. Qed.
 
-  Local Hint Resolve nf1 nf2 nf_a1 nf_a2 nf_b1 nf_b2 : T2.
+  #[local] Hint Resolve nf1 nf2 nf_a1 nf_a2 nf_b1 nf_b2 : T2.
 
   Remark nf_c1 : nf c1.
   Proof.  nf_inv.  Qed.
@@ -1615,7 +1615,7 @@ Section lt_incl_rpo.
   Remark nf_c2 : nf c2.
   Proof. nf_inv.  Qed.
 
-  Local Hint Resolve nf_c1 nf_c2 : T2.
+  #[local] Hint Resolve nf_c1 nf_c2 : T2.
 
   Hypothesis H : gcons a1 b1 n1 c1 t2< gcons a2 b2 n2 c2.
 
@@ -1903,14 +1903,14 @@ Proof.
   split; destruct y; try contradiction.
 Qed.
 
-Global Hint Resolve R1 : T2.
+#[global] Hint Resolve R1 : T2.
 
 Remark R2 : Acc P.prec ord_zero.
 Proof.
   split; destruct y; try contradiction; auto with T2.
 Qed.
 
-Global Hint Resolve R2 : T2.
+#[global] Hint Resolve R2 : T2.
 
 Remark R3 : Acc P.prec nat_S.
 Proof.
@@ -1918,21 +1918,21 @@ Proof.
 Qed.
 
 
-Global Hint Resolve R3 : T2.
+#[global] Hint Resolve R3 : T2.
 
 Remark R4 : Acc P.prec ord_cons.
 Proof.
   split; destruct y; try contradiction;auto with T2.
 Qed.
 
-Global Hint Resolve R4 : T2.
+#[global] Hint Resolve R4 : T2.
 
 Remark R5 : Acc P.prec ord_psi.
 Proof.
   split; destruct y; try contradiction;auto with T2.
 Qed.
 
-Global Hint Resolve R5 : T2.
+#[global] Hint Resolve R5 : T2.
 
 Theorem well_founded_rpo : well_founded rpo.
 Proof.
@@ -1944,7 +1944,7 @@ Section  well_founded.
   
   Let R := restrict  nf lt.
 
-  Local Hint Unfold restrict R : T2.
+  #[local] Hint Unfold restrict R : T2.
 
   Lemma R_inc_rpo : forall o o', R o o' -> rpo (T2_2_term o) (T2_2_term o').
   Proof.
@@ -3790,7 +3790,7 @@ Qed.
 
   Coercion Finite : nat >-> G0.
 
-  Local Open Scope g0_scope.
+  #[local] Open Scope g0_scope.
 
   Example Ex42 : omega + 42 + omega^ 2 = omega^ 2.
   Proof.
diff --git a/theories/ordinals/Gamma0/T2.v b/theories/ordinals/Gamma0/T2.v
index 17be6c16..de9345ab 100644
--- a/theories/ordinals/Gamma0/T2.v
+++ b/theories/ordinals/Gamma0/T2.v
@@ -69,7 +69,7 @@ Inductive is_finite:  T2 ->  Set :=
  zero_finite : is_finite zero
 |succ_finite : forall n, is_finite (gcons zero zero n zero).
 
-Global Hint Constructors is_finite : T2.
+#[global] Hint Constructors is_finite : T2.
 
 
 
@@ -235,7 +235,7 @@ Inductive nf : T2 -> Prop :=
     nf(gcons a' b' n' c')-> 
     nf(gcons a b n (gcons a' b' n' c')).
 
-Global Hint Constructors nf : T2. 
+#[global] Hint Constructors nf : T2. 
 
 (* end snippet nfDef *)
 
diff --git a/theories/ordinals/Hydra/Epsilon0_Needed_Generic.v b/theories/ordinals/Hydra/Epsilon0_Needed_Generic.v
index efec2eab..d02a79de 100644
--- a/theories/ordinals/Hydra/Epsilon0_Needed_Generic.v
+++ b/theories/ordinals/Hydra/Epsilon0_Needed_Generic.v
@@ -27,7 +27,7 @@ Section Bounded.
   Lemma  nf_m : forall h, nf (m h).
   Proof. intro h0; now destruct (m_bounded h0). Qed.
 
-  Local Hint Resolve Rem0 : hydra.
+  #[local] Hint Resolve Rem0 : hydra.
   
 
 
diff --git a/theories/ordinals/Hydra/Hydra_Termination.v b/theories/ordinals/Hydra/Hydra_Termination.v
index d8bc27bb..3fccb1b3 100644
--- a/theories/ordinals/Hydra/Hydra_Termination.v
+++ b/theories/ordinals/Hydra/Hydra_Termination.v
@@ -197,7 +197,7 @@ Qed.
 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.
diff --git a/theories/ordinals/Hydra/Omega_Small.v b/theories/ordinals/Hydra/Omega_Small.v
index 73540237..ee45ab73 100644
--- a/theories/ordinals/Hydra/Omega_Small.v
+++ b/theories/ordinals/Hydra/Omega_Small.v
@@ -80,7 +80,7 @@ Section Impossibility_Proof.
 
 (* end snippet smallHDef *)
 
-  Local Hint Resolve big_to_small : hydra.
+  #[local] Hint Resolve big_to_small : hydra.
 
 
   (* begin snippet mLt *)
diff --git a/theories/ordinals/OrdinalNotations/ON_Generic.v b/theories/ordinals/OrdinalNotations/ON_Generic.v
index 557e30cf..68671be7 100644
--- a/theories/ordinals/OrdinalNotations/ON_Generic.v
+++ b/theories/ordinals/OrdinalNotations/ON_Generic.v
@@ -14,7 +14,7 @@ Require Export Comparable.
 Generalizable All Variables.
 Declare Scope ON_scope.
 Delimit Scope ON_scope with on.
-Local Open Scope ON_scope.
+#[local] Open Scope ON_scope.
 
 (**
   Ordinal notation system on type [A] :
@@ -77,7 +77,7 @@ Infix "o?=" := ON_compare (at level 70) : ON_scope.
 
 (* end snippet ONDefsb *)
 
-Global Hint Resolve wf_measure : core.
+#[global] Hint Resolve wf_measure : core.
 
 (** The segment associated with nA is isomorphic to
     the segment of ordinals strictly less than b *)
diff --git a/theories/ordinals/OrdinalNotations/ON_Omega.v b/theories/ordinals/OrdinalNotations/ON_Omega.v
index 175244fb..5215dcc2 100644
--- a/theories/ordinals/OrdinalNotations/ON_Omega.v
+++ b/theories/ordinals/OrdinalNotations/ON_Omega.v
@@ -47,9 +47,8 @@ Defined.
 
 
 
-Global Instance FinOrd_Omega (i:nat) :
-  SubON (FinOrd i) Omega i 
-             (fun alpha =>  proj1_sig alpha).
+#[global] Instance FinOrd_Omega (i:nat) :
+  SubON (FinOrd i) Omega i (fun alpha =>  proj1_sig alpha).
 Proof.
   split.
   - reflexivity.
diff --git a/theories/ordinals/OrdinalNotations/ON_Omega2.v b/theories/ordinals/OrdinalNotations/ON_Omega2.v
index e235fcaa..5f065b0c 100644
--- a/theories/ordinals/OrdinalNotations/ON_Omega2.v
+++ b/theories/ordinals/OrdinalNotations/ON_Omega2.v
@@ -119,8 +119,8 @@ Qed.
 
 (* end snippet succLemmas *)
 
-Global Hint Constructors clos_refl lexico : O2.
-Global Hint Unfold lt le : O2.
+#[global] Hint Constructors clos_refl lexico : O2.
+#[global] Hint Unfold lt le : O2.
 
 
 
@@ -567,7 +567,7 @@ Section Merge.
 
   Variable A: Type.
 
-  Local Definition m (p : list A * list A) :=
+  #[local] Definition m (p : list A * list A) :=
     omega * length (fst p) + length (snd p).
 
   Function  merge  (ltb: A -> A -> bool)
diff --git a/theories/ordinals/OrdinalNotations/ON_plus.v b/theories/ordinals/OrdinalNotations/ON_plus.v
index e37095a0..f9b68d3b 100644
--- a/theories/ordinals/OrdinalNotations/ON_plus.v
+++ b/theories/ordinals/OrdinalNotations/ON_plus.v
@@ -42,8 +42,8 @@ fun (alpha beta: t) =>
 
 Definition le := clos_refl _ lt.
 
-Local Hint Unfold lt le : core.
-Local Hint Constructors le_AsB: core.
+#[local] Hint Unfold lt le : core.
+#[local] Hint Constructors le_AsB: core.
 
 Instance lt_strorder : StrictOrder lt.
 Proof.
diff --git a/theories/ordinals/Prelude/Comparable.v b/theories/ordinals/Prelude/Comparable.v
index 789a32eb..0ef0e19f 100644
--- a/theories/ordinals/Prelude/Comparable.v
+++ b/theories/ordinals/Prelude/Comparable.v
@@ -467,7 +467,7 @@ Section Comparable.
 
 End Comparable.
 
-Local Ltac compare_trans H1 H2 intropattern :=
+#[local] Ltac compare_trans H1 H2 intropattern :=
   lazymatch type of (H1, H2) with
   | ((?compare ?a ?b = ?comp_res) * (?compare ?b ?c = ?comp_res))%type =>
     assert (compare a c = comp_res) as intropattern by
diff --git a/theories/ordinals/Prelude/DecPreOrder_Instances.v b/theories/ordinals/Prelude/DecPreOrder_Instances.v
index 75daafb6..53c6d9f1 100644
--- a/theories/ordinals/Prelude/DecPreOrder_Instances.v
+++ b/theories/ordinals/Prelude/DecPreOrder_Instances.v
@@ -109,7 +109,7 @@ Inductive lex_prod (p p':A*B): Prop :=
 Notation "x '<=lex' y" := (lex_prod x y) (at level 70, no associativity).
 Notation "x '<lex' y" := (@lt (A*B)  lex_prod _ x y) (at level 70, no associativity).
 
- Global Instance PO_lex_prod : PreOrder lex_prod.
+ #[global] Instance PO_lex_prod : PreOrder lex_prod.
  Proof.
  split.
  -   intro x; right;  reflexivity.
@@ -179,7 +179,7 @@ Proof.
   apply (lex_inv_left _ _ _ _ H0).
 Qed.
 
-Global Instance To_lex_prod : TotalPreOrder lex_prod.
+#[global] Instance To_lex_prod : TotalPreOrder lex_prod.
 Proof.
   split.
   - apply PO_lex_prod.
@@ -199,7 +199,7 @@ Proof.
         { left;  right;[ now symmetry | assumption]. }
 Qed.
 
-Global Instance lex_prod_dec : RelDecision lex_prod.
+#[global] Instance lex_prod_dec : RelDecision lex_prod.
 Proof.
 intros x y; destruct x, y.
 destruct (decide (leA a a0)) as [HAle|Hale].
diff --git a/theories/ordinals/Prelude/Fuel.v b/theories/ordinals/Prelude/Fuel.v
index a3791574..02a02e53 100644
--- a/theories/ordinals/Prelude/Fuel.v
+++ b/theories/ordinals/Prelude/Fuel.v
@@ -2,12 +2,11 @@
 (* Robert Krebbers's trick  *)
 
 Require Import FunInd Recdef Wf_nat Lia.
-Import Nat.
 
 Function zero (n:nat)  {wf lt n} : nat :=
   match n with
     0 => 0
-  | p => zero (div2 p)
+  | p => zero (Nat.div2 p)
   end.
 Proof.
   intros; apply PeanoNat.Nat.lt_div2; auto with arith.
@@ -35,7 +34,7 @@ Qed.
   Function zero (n:nat)  {wf lt n} : nat :=
     match n with
       0 => 0
-    | p => zero (div2 p)
+    | p => zero (Nat.div2 p)
     end.
   Proof.
     intros;  apply PeanoNat.Nat.lt_div2; auto with arith.
@@ -71,7 +70,7 @@ Compute Acc_intro_generator 2 lt_wf  42.
 Function zero' (n:nat)  {wf lt n} : nat :=
   match n with
     0 => 0
-  | p => zero' (div2 p)
+  | p => zero' (Nat.div2 p)
   end.
 Proof.
   intros; apply PeanoNat.Nat.lt_div2;  auto with arith.
diff --git a/theories/ordinals/Prelude/LibHyps_Experiments.v b/theories/ordinals/Prelude/LibHyps_Experiments.v
index a10afb48..0edf3703 100644
--- a/theories/ordinals/Prelude/LibHyps_Experiments.v
+++ b/theories/ordinals/Prelude/LibHyps_Experiments.v
@@ -5,7 +5,7 @@ Require Export MoreLibHyps.
 
 Require Import List.
 Import ListNotations. 
-Local Open Scope autonaming_scope.
+#[local] Open Scope autonaming_scope.
 
 Ltac rename_hyp n th ::= rename_short n th.
 
diff --git a/theories/ordinals/Prelude/MoreLists.v b/theories/ordinals/Prelude/MoreLists.v
index ff50f076..dca81a79 100644
--- a/theories/ordinals/Prelude/MoreLists.v
+++ b/theories/ordinals/Prelude/MoreLists.v
@@ -274,7 +274,7 @@ Qed.
 
 
 
-Global Hint Constructors sorted_ge : lists.
+#[global] Hint Constructors sorted_ge : lists.
 
 
 Lemma sorted_inv_gt : forall n p s, sorted_ge n (p::s) ->
diff --git a/theories/ordinals/Prelude/MoreVectors.v b/theories/ordinals/Prelude/MoreVectors.v
index 16bd54c8..4dd1d367 100644
--- a/theories/ordinals/Prelude/MoreVectors.v
+++ b/theories/ordinals/Prelude/MoreVectors.v
@@ -1,5 +1,4 @@
 Require Export Bool Arith Vector Lia.
-Import PeanoNat.Nat. 
 Import Vector VectorNotations.
 
 (** generalities on vectors *)
@@ -248,7 +247,7 @@ Lemma max_v_2 : forall x y,  max_v (x::y::nil) = max x y. (* .no-out *)
 (* end snippet maxvLemmasa *)
 
 Proof.
-  intros; cbn. now rewrite max_0_r.
+  intros; cbn. now rewrite Max.max_0_r.
 Qed.
 
 (* begin snippet maxvLemmasb *)
@@ -264,7 +263,8 @@ Proof.
   -  intros v; rewrite (t_0_nil _ v); cbn.
      intros; auto with arith.
   -   intros v; rewrite (decomp _ _ v); cbn.
-      intros;  destruct (Forall_inv _ _ _  _ H). apply max_lub; auto. 
+      intros;  destruct (Forall_inv _ _ _  _ H).
+      apply Max.max_lub; auto. 
 Qed.
 
 (* begin snippet maxvLemmasc *)
@@ -278,7 +278,7 @@ Proof.
   induction n.  
   -  intros v; rewrite (t_0_nil _ v); cbn; inversion 1.
   -  intros v; rewrite (decomp _ _ v); cbn; intros; destruct (In_cases _ _ H).
-     +  cbn in H0; subst; apply le_max_l. 
+     +  cbn in H0; subst; apply Max.le_max_l. 
      + cbn in H0; specialize (IHn _ _ H0); lia.
 Qed.
 
@@ -286,7 +286,7 @@ Qed.
 Lemma max_v_tl {n:nat}(v:  Vector.t nat (S n)) :
   max_v (Vector.tl v) <= max_v v.
 Proof.
-  rewrite (decomp _ _ v);  cbn;  apply le_max_r.
+  rewrite (decomp _ _ v);  cbn;  apply Max.le_max_r.
 Qed.
 
 (*
diff --git a/theories/ordinals/Prelude/Sort_spec.v b/theories/ordinals/Prelude/Sort_spec.v
index 129a25d0..81bf12b1 100644
--- a/theories/ordinals/Prelude/Sort_spec.v
+++ b/theories/ordinals/Prelude/Sort_spec.v
@@ -47,7 +47,7 @@ Definition sort_correct  (f: list A -> list A) : Prop :=
 Definition equiv (x y : A) := R x  y /\ R y  x.
 
 
-Global Instance equiv_equiv (P: PreOrder R): Equivalence equiv.
+#[global] Instance equiv_equiv (P: PreOrder R): Equivalence equiv.
 Proof. 
 split.
 - intro x;split;reflexivity.
@@ -126,7 +126,7 @@ End R_given.
 
 
 Arguments LocallySorted {A} _ _.
-Global Hint Constructors LocallySorted : lists.
+#[global] Hint Constructors LocallySorted : lists.
 
 (** A sort must work on any decidable total pre-order *)
 
diff --git a/theories/ordinals/Schutte/AP.v b/theories/ordinals/Schutte/AP.v
index bf518a53..a5324b7b 100644
--- a/theories/ordinals/Schutte/AP.v
+++ b/theories/ordinals/Schutte/AP.v
@@ -122,7 +122,7 @@ Qed.
 
 
 
-Global Hint Resolve zero_lt_omega : schutte.
+#[global] Hint Resolve zero_lt_omega : schutte.
 
 Lemma AP_finite_eq_one : forall n: nat, AP n -> n = 1.
 Proof with auto with schutte.
@@ -234,7 +234,7 @@ Section AP_Unbounded.
       
   Qed.
 
-  Local Hint Resolve mono_seq mono_seq2 : schutte.
+  #[local] Hint Resolve mono_seq mono_seq2 : schutte.
 
 
   Remark alpha_lt_beta : alpha < beta.
diff --git a/theories/ordinals/Schutte/CNF.v b/theories/ordinals/Schutte/CNF.v
index 46fd0979..e1119b83 100644
--- a/theories/ordinals/Schutte/CNF.v
+++ b/theories/ordinals/Schutte/CNF.v
@@ -52,8 +52,8 @@ Definition exponents_le (alpha : Ord) :=
 
 (* begin hide *)
 
-Global Hint Constructors LocallySorted : schutte.
-Global Hint Unfold sorted : schutte.
+#[global] Hint Constructors LocallySorted : schutte.
+#[global] Hint Unfold sorted : schutte.
 
 (* end hide *)
 
diff --git a/theories/ordinals/Schutte/Ordering_Functions.v b/theories/ordinals/Schutte/Ordering_Functions.v
index 9eeff987..a03195a0 100644
--- a/theories/ordinals/Schutte/Ordering_Functions.v
+++ b/theories/ordinals/Schutte/Ordering_Functions.v
@@ -137,7 +137,7 @@ Lemma ordering_function_mono (f : Ord -> Ord) (A B: Ensemble Ord) :
     In A alpha -> In A beta -> alpha < beta -> f alpha < f beta.
 Proof.  now destruct 1. Qed.
 
-Global Hint Resolve ordering_function_mono : schutte.
+#[global] Hint Resolve ordering_function_mono : schutte.
 
 Lemma  ordering_function_mono_weak (f : Ord -> Ord) (A B: Ensemble Ord) : 
  ordering_function f A B ->
@@ -149,7 +149,7 @@ Proof.
  -  right;auto.
 Qed.
 
-Global Hint Resolve ordering_function_mono_weak : schutte.
+#[global] Hint Resolve ordering_function_mono_weak : schutte.
 
 Lemma ordering_function_monoR : forall f A B, ordering_function f A B ->
    forall a b, In A a -> In A b -> f a < f b -> a < b.
@@ -160,7 +160,7 @@ Proof.
   - destruct (@lt_irrefl (f a)); apply lt_trans with (f b); auto.
 Qed.
 
-Global Hint Resolve ordering_function_monoR : schutte.
+#[global] Hint Resolve ordering_function_monoR : schutte.
 
 
 Lemma Ordering_bijection : forall f A B, ordering_function f A B ->
@@ -188,7 +188,7 @@ Proof with auto with schutte.
   -  right; eapply ordering_function_monoR; eauto.
 Qed.
 
-Global Hint Resolve ordering_function_mono_weakR : schutte.
+#[global] Hint Resolve ordering_function_mono_weakR : schutte.
 
 
 Lemma ordering_function_seg : forall A B, ordering_segment A B ->
@@ -264,7 +264,7 @@ Section ordering_function_unicity_1.
  Remark SA2 : segment A2.
  Proof.  case O2;intuition.  Qed.
  
- Local Hint Resolve SA2 SA1 : schutte.
+ #[local] Hint Resolve SA2 SA1 : schutte.
 
   Lemma A1_A2 :forall a, In A1 a -> A2 a /\ f1 a = f2 a.
  Proof with eauto with schutte.
@@ -468,7 +468,7 @@ Section building_ordering_function_1.
   apply AX2; exists beta;  destruct 1;tauto.
  Qed.
 
- Local Hint Resolve of_beta': schutte.
+ #[local] Hint Resolve of_beta': schutte.
 
 Remark A_denum : countable _A.
 Proof.
@@ -670,7 +670,7 @@ Qed.
       case (@lt_irrefl _ H2).
  Qed.
 
- Local Hint Resolve g_bij : schutte.
+ #[local] Hint Resolve g_bij : schutte.
 
 
 Let g_1 := inv_fun inh_Ord B (image B g) g.
@@ -680,7 +680,7 @@ Proof.
  unfold  g_1; apply inv_fun_bij; auto with schutte.
 Qed.
 
-Local Hint Resolve g_1_bij : schutte.
+#[local] Hint Resolve g_1_bij : schutte.
 
 
 Lemma g_1_of : ordering_function g_1 (image B g) B.
@@ -1032,7 +1032,7 @@ Proof with eauto with schutte.
 Qed.
 
 
-Local Hint Resolve  alpha_A : schutte.
+#[local] Hint Resolve  alpha_A : schutte.
  
 Remark R7 : |_| U <= alpha_ .
 Proof. 
diff --git a/theories/ordinals/Schutte/Schutte_basics.v b/theories/ordinals/Schutte/Schutte_basics.v
index 77d00354..95b42c5f 100644
--- a/theories/ordinals/Schutte/Schutte_basics.v
+++ b/theories/ordinals/Schutte/Schutte_basics.v
@@ -18,7 +18,7 @@ Declare Scope schutte_scope.
 
 Set Implicit Arguments.
 
-Global Hint Unfold In : schutte.
+#[global] Hint Unfold In : schutte.
 Arguments Included [U] _ _.
 Arguments countable [U] _.
 Arguments Same_set [U] _ _.
@@ -39,7 +39,7 @@ Infix "<" := lt : schutte_scope.
 Definition ordinal : Ensemble Ord := Full_set Ord.
 Definition big0 alpha : Ensemble Ord := fun beta =>  beta < alpha.
 
-Global Hint Unfold ordinal : schutte.
+#[global] Hint Unfold ordinal : schutte.
 
 (* end snippet OrdDecl *)
 
@@ -51,7 +51,7 @@ Qed.
 
 (* end hide *)
 
-Global Hint Resolve ordinal_ok : schutte. 
+#[global] Hint Resolve ordinal_ok : schutte. 
 
 (** * The three axioms by Schutte *)
 
@@ -63,9 +63,9 @@ Axiom AX1 : WO lt.
 (* end snippet AX1 *)
 
 
-Global Hint Resolve AX1 : schutte. 
+#[global] Hint Resolve AX1 : schutte. 
 
-Global Instance WO_ord : WO  lt := AX1.
+#[global] Instance WO_ord : WO  lt := AX1.
 
 (** Stuff for using Coq.Logic.Epsilon *)
 (* begin snippet inhOrd *)  
@@ -91,7 +91,7 @@ Qed.
 
 
 
-Global Hint Resolve  AX1 Inh_Ord_Ord Inh_OSets inh_Ord : schutte.
+#[global] Hint Resolve  AX1 Inh_Ord_Ord Inh_OSets inh_Ord : schutte.
 
 Definition le := Le lt.
 
@@ -277,7 +277,7 @@ Proof.
   left;auto.
 Qed.
 
-Global Hint Resolve le_refl : schutte.
+#[global] Hint Resolve le_refl : schutte.
 
 Lemma eq_le : forall a b : Ord,  a = b -> a <= b.
 Proof.
@@ -326,7 +326,7 @@ Proof.
   -  intros H0 H1;case (@lt_irrefl a);eapply lt_trans;eauto.
 Qed.
 
-Global Hint Resolve eq_le lt_le lt_trans le_trans le_lt_trans 
+#[global] Hint Resolve eq_le lt_le lt_trans le_trans le_lt_trans 
      lt_le_trans lt_irrefl le_not_gt:
   schutte.
 
@@ -370,7 +370,7 @@ Proof.
   intros a b  H1; tricho a b H2; auto with schutte;  contradiction.  
 Qed.
 
-Global Hint Unfold Included : schutte.
+#[global] Hint Unfold Included : schutte.
 
 (** ** Global properties *)
 
@@ -577,7 +577,7 @@ Qed.
 
 (* end snippet succProps *)
 
-Global Hint Resolve zero_lt_succ zero_le : schutte.
+#[global] Hint Resolve zero_lt_succ zero_le : schutte.
 
 (** Less than finite is finite ... *)
 
@@ -602,7 +602,7 @@ Proof.
      simpl (finite (S m)); apply lt_succ; auto with schutte.
 Qed.
 
-Global Hint Resolve finite_mono : schutte.
+#[global] Hint Resolve finite_mono : schutte.
 
 Lemma finite_inj : forall i j, F i = F j -> i = j.
 Proof.
@@ -852,13 +852,13 @@ Proof.
     rewrite H0;intro;case (@Lt_irreflexive  Ord lt AX1 (s j));auto.
 Qed.
 
-Global Hint Resolve Countable.seq_range_countable seq_mono_intro : schutte.
+#[global] Hint Resolve Countable.seq_range_countable seq_mono_intro : schutte.
 
 
 Lemma In_full {A:Type} (a:A) : In (Full_set A ) a.
 Proof. split. Qed.
 
-Global Hint Resolve In_full: core.
+#[global] Hint Resolve In_full: core.
 
 Lemma lt_omega_limit (s : nat -> Ord) :
   seq_mono s -> forall i, s i <  omega_limit s.
@@ -993,7 +993,7 @@ Proof.
  apply AX2;   now exists alpha.
 Qed.
 
-Global Hint Resolve countable_members : schutte.
+#[global] Hint Resolve countable_members : schutte.
 
 Lemma le_sup_members (alpha : Ord) :  |_| (members alpha) <= alpha.
 Proof.
diff --git a/theories/ordinals/Schutte/Well_Orders.v b/theories/ordinals/Schutte/Well_Orders.v
index e34c5547..914b5687 100644
--- a/theories/ordinals/Schutte/Well_Orders.v
+++ b/theories/ordinals/Schutte/Well_Orders.v
@@ -13,7 +13,7 @@ Arguments In [U].
 Arguments Included [U].
 
 Set Implicit Arguments.
-Global Hint Unfold In : core.
+#[global] Hint Unfold In : core.
 
 
 Section the_context.
@@ -72,7 +72,7 @@ Section the_context.
       - intros;case (Lt_irreflexive (a:=a)); eapply (Lt_trans );eauto. 
     Qed.
 
-    Global Instance  Le_trans : Transitive  Le. 
+    #[global] Instance  Le_trans : Transitive  Le. 
     Proof.
       unfold Transitive, Le;intros.
       case H;case H0.
diff --git a/theories/ordinals/rpo/list_permut.v b/theories/ordinals/rpo/list_permut.v
index 0d0c4d46..6cc868cc 100644
--- a/theories/ordinals/rpo/list_permut.v
+++ b/theories/ordinals/rpo/list_permut.v
@@ -98,8 +98,8 @@ Proof.
 unfold list_permut, meq; intros; apply sym_eq; trivial.
 Qed.
 
-Global Hint Immediate list_permut_refl : core.
-Global Hint Resolve list_permut_sym : core.
+#[global] Hint Immediate list_permut_refl : core.
+#[global] Hint Resolve list_permut_sym : core.
 
 (** Transitivity. *)
 Theorem list_permut_trans :