Mercurial > cpdt > repo
diff src/Large.v @ 426:5f25705a10ea
Pass through DataStruct, to incorporate new coqdoc features; globally replace [refl_equal] with [eq_refl]
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 25 Jul 2012 18:10:26 -0400 |
| parents | 6f0f80ffd5b6 |
| children | 5eebaaa9f952 |
line wrap: on
line diff
--- a/src/Large.v Wed Jul 25 17:50:12 2012 -0400 +++ b/src/Large.v Wed Jul 25 18:10:26 2012 -0400 @@ -565,13 +565,13 @@ (** %\vspace{-.15in}%[[ == intro x; intro y; intro H; intro H0; intro H4; simple eapply trans_eq. - simple apply refl_equal. + simple apply eq_refl. simple eapply trans_eq. - simple apply refl_equal. + simple apply eq_refl. simple eapply trans_eq. - simple apply refl_equal. + simple apply eq_refl. simple apply H1. eexact H. @@ -596,20 +596,20 @@ 1.1.1.1.1.1 depth=6 intro 1.1.1.1.1.1.1 depth=5 apply H3 1.1.1.1.1.1.1.1 depth=4 eapply trans_eq -1.1.1.1.1.1.1.1.1 depth=4 apply refl_equal +1.1.1.1.1.1.1.1.1 depth=4 apply eq_refl 1.1.1.1.1.1.1.1.1.1 depth=3 eapply trans_eq -1.1.1.1.1.1.1.1.1.1.1 depth=3 apply refl_equal +1.1.1.1.1.1.1.1.1.1.1 depth=3 apply eq_refl 1.1.1.1.1.1.1.1.1.1.1.1 depth=2 eapply trans_eq -1.1.1.1.1.1.1.1.1.1.1.1.1 depth=2 apply refl_equal +1.1.1.1.1.1.1.1.1.1.1.1.1 depth=2 apply eq_refl 1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=1 eapply trans_eq -1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=1 apply refl_equal +1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=1 apply eq_refl 1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=0 eapply trans_eq 1.1.1.1.1.1.1.1.1.1.1.1.1.1.2 depth=1 apply sym_eq ; trivial 1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1 depth=0 eapply trans_eq 1.1.1.1.1.1.1.1.1.1.1.1.1.1.3 depth=0 eapply trans_eq 1.1.1.1.1.1.1.1.1.1.1.1.2 depth=2 apply sym_eq ; trivial 1.1.1.1.1.1.1.1.1.1.1.1.2.1 depth=1 eapply trans_eq -1.1.1.1.1.1.1.1.1.1.1.1.2.1.1 depth=1 apply refl_equal +1.1.1.1.1.1.1.1.1.1.1.1.2.1.1 depth=1 apply eq_refl 1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1 depth=0 eapply trans_eq 1.1.1.1.1.1.1.1.1.1.1.1.2.1.2 depth=1 apply sym_eq ; trivial 1.1.1.1.1.1.1.1.1.1.1.1.2.1.2.1 depth=0 eapply trans_eq