fix a conflict

coq-community · Jan 26, 2024 · 592a1fe · 592a1fe
2 parents e4b655c + 11b82b1
commit 592a1fe
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/theories/ordinals/Epsilon0/Canon.v b/theories/ordinals/Epsilon0/Canon.v
@@ -1033,7 +1033,7 @@ Lemma CanonSSn (i:nat) :
                     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.
+   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.