Minor corrections

Author: Casteran

doc/ordinal-chapter.tex

@@ -924,7 +924,7 @@ \subsubsection{Building an instance of \texttt{ON}}
  There is no interesting arithmetic on finite ordinals, since functions like successor, addition, etc.,  cannot be represented in \coq{} as \emph{total} functions.
 \end{remark}
 
-\section{See also \dots}
+\subsubsection{See also \dots}
 
 \gaiasign Finite ordinals are also formalized in \ssreflect/\mathcomp~\cite{MCB}. In Module~\href{../theories/html/gaia_hydras.ON_gfinite.html}{gaia\_hydras.ON\_gfinite}, we build an instance of class \texttt{ON}.
 
@@ -936,7 +936,7 @@ \section{See also \dots}
 
 
 
-  See also Adam Chlipala's \emph{CPDT}~\cite{chlipalacpdt2011} for a thorough study of the use of dependent types.  
+ 
 
 
 

theories/ordinals/OrdinalNotations/ON_Generic.v

@@ -24,8 +24,9 @@ Delimit Scope ON_scope with on.
 Class ON {A:Type} (lt: relation A) (cmp: Compare A) :=
   {
   ON_comp :> Comparable lt cmp;
-  ON_wf :> well_founded lt;
+  ON_wf : well_founded lt;
   }.
+
 #[global] Existing Instance ON_comp.
 Coercion ON_wf :  ON >-> well_founded.
 
@@ -94,8 +95,8 @@ Class  SubON
   {
     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}.
+    SubON_incl : forall x, ltB (iota x) alpha;
+    SubON_onto : forall y, ltB y alpha  -> exists x:A, iota x = y}.
 
 (* end snippet SubONDef *)