Projection (#175)

* minor change

* Data type associated with an ordinal notation is now a coercio

Author: Casteran

theories/ordinals/Epsilon0/Canon.v

@@ -1032,9 +1032,9 @@ Lemma CanonSSn (i:nat) :
                     Canon (Cons alpha (S n) E0zero) (S i) =
                     Cons alpha n (Canon (E0_phi0 alpha) (S i)).
 Proof.
-  intros; apply E0_eq_intro;
-   unfold Canon;repeat (rewrite cnf_rw || rewrite cnf_Cons); auto.
-  - rewrite canon_SSn_zero; auto with E0.
+  intros; apply E0_eq_intro.
+  unfold Canon;  repeat (rewrite cnf_rw || rewrite cnf_Cons); auto.
+  -  rewrite canon_SSn_zero; auto with E0.
   -  unfold lt, E0_phi0; repeat rewrite cnf_rw. 
      apply canonS_LT ; trivial. 
      apply nf_phi0;auto with E0. 

theories/ordinals/Hydra/Omega2_Small.v

@@ -19,7 +19,7 @@ Section Impossibility_Proof.
 
   (* begin snippet Impossibilitya *)
 
-  Variable m : Hydra -> ON_Omega2.t.
+  Variable m : Hydra -> rep Omega2.
   Context
     (Hvar: Hvariant Omega2 free m).
 

theories/ordinals/OrdinalNotations/ON_Generic.v

@@ -30,6 +30,10 @@ Class ON {A:Type} (lt: relation A) (cmp: Compare A) :=
 #[global] Existing Instance ON_comp.
 Coercion ON_wf :  ON >-> well_founded.
 
+Definition rep {A:Type} {lt: relation A} {cmp: Compare A}
+                (on : ON lt cmp) := A. 
+
+#[global] Coercion rep : ON >-> Sortclass.
 (* end snippet ONDef *)
 
 (* begin snippet ONDefsa:: no-out  *)

theories/ordinals/OrdinalNotations/ON_Omega2.v

@@ -498,7 +498,6 @@ Proof.
  - abstract lia.
 Qed.
 
-
 Lemma ap_cases alpha : ap alpha -> alpha = 1 \/ alpha = omega.
 Proof.
   destruct (zero_limit_succ_dec alpha) as [[Hzero |  Hlim] | Hsucc].