Mercurial > cpdt > repo
comparison 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 |
comparison
equal
deleted
inserted
replaced
425:6ed5ee4845e4 | 426:5f25705a10ea |
---|---|
563 Restart. | 563 Restart. |
564 info eauto 6. | 564 info eauto 6. |
565 (** %\vspace{-.15in}%[[ | 565 (** %\vspace{-.15in}%[[ |
566 == intro x; intro y; intro H; intro H0; intro H4; | 566 == intro x; intro y; intro H; intro H0; intro H4; |
567 simple eapply trans_eq. | 567 simple eapply trans_eq. |
568 simple apply refl_equal. | 568 simple apply eq_refl. |
569 | 569 |
570 simple eapply trans_eq. | 570 simple eapply trans_eq. |
571 simple apply refl_equal. | 571 simple apply eq_refl. |
572 | 572 |
573 simple eapply trans_eq. | 573 simple eapply trans_eq. |
574 simple apply refl_equal. | 574 simple apply eq_refl. |
575 | 575 |
576 simple apply H1. | 576 simple apply H1. |
577 eexact H. | 577 eexact H. |
578 | 578 |
579 eexact H0. | 579 eexact H0. |
594 1.1.1.1 depth=6 intro | 594 1.1.1.1 depth=6 intro |
595 1.1.1.1.1 depth=6 intro | 595 1.1.1.1.1 depth=6 intro |
596 1.1.1.1.1.1 depth=6 intro | 596 1.1.1.1.1.1 depth=6 intro |
597 1.1.1.1.1.1.1 depth=5 apply H3 | 597 1.1.1.1.1.1.1 depth=5 apply H3 |
598 1.1.1.1.1.1.1.1 depth=4 eapply trans_eq | 598 1.1.1.1.1.1.1.1 depth=4 eapply trans_eq |
599 1.1.1.1.1.1.1.1.1 depth=4 apply refl_equal | 599 1.1.1.1.1.1.1.1.1 depth=4 apply eq_refl |
600 1.1.1.1.1.1.1.1.1.1 depth=3 eapply trans_eq | 600 1.1.1.1.1.1.1.1.1.1 depth=3 eapply trans_eq |
601 1.1.1.1.1.1.1.1.1.1.1 depth=3 apply refl_equal | 601 1.1.1.1.1.1.1.1.1.1.1 depth=3 apply eq_refl |
602 1.1.1.1.1.1.1.1.1.1.1.1 depth=2 eapply trans_eq | 602 1.1.1.1.1.1.1.1.1.1.1.1 depth=2 eapply trans_eq |
603 1.1.1.1.1.1.1.1.1.1.1.1.1 depth=2 apply refl_equal | 603 1.1.1.1.1.1.1.1.1.1.1.1.1 depth=2 apply eq_refl |
604 1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=1 eapply trans_eq | 604 1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=1 eapply trans_eq |
605 1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=1 apply refl_equal | 605 1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=1 apply eq_refl |
606 1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=0 eapply trans_eq | 606 1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 depth=0 eapply trans_eq |
607 1.1.1.1.1.1.1.1.1.1.1.1.1.1.2 depth=1 apply sym_eq ; trivial | 607 1.1.1.1.1.1.1.1.1.1.1.1.1.1.2 depth=1 apply sym_eq ; trivial |
608 1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1 depth=0 eapply trans_eq | 608 1.1.1.1.1.1.1.1.1.1.1.1.1.1.2.1 depth=0 eapply trans_eq |
609 1.1.1.1.1.1.1.1.1.1.1.1.1.1.3 depth=0 eapply trans_eq | 609 1.1.1.1.1.1.1.1.1.1.1.1.1.1.3 depth=0 eapply trans_eq |
610 1.1.1.1.1.1.1.1.1.1.1.1.2 depth=2 apply sym_eq ; trivial | 610 1.1.1.1.1.1.1.1.1.1.1.1.2 depth=2 apply sym_eq ; trivial |
611 1.1.1.1.1.1.1.1.1.1.1.1.2.1 depth=1 eapply trans_eq | 611 1.1.1.1.1.1.1.1.1.1.1.1.2.1 depth=1 eapply trans_eq |
612 1.1.1.1.1.1.1.1.1.1.1.1.2.1.1 depth=1 apply refl_equal | 612 1.1.1.1.1.1.1.1.1.1.1.1.2.1.1 depth=1 apply eq_refl |
613 1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1 depth=0 eapply trans_eq | 613 1.1.1.1.1.1.1.1.1.1.1.1.2.1.1.1 depth=0 eapply trans_eq |
614 1.1.1.1.1.1.1.1.1.1.1.1.2.1.2 depth=1 apply sym_eq ; trivial | 614 1.1.1.1.1.1.1.1.1.1.1.1.2.1.2 depth=1 apply sym_eq ; trivial |
615 1.1.1.1.1.1.1.1.1.1.1.1.2.1.2.1 depth=0 eapply trans_eq | 615 1.1.1.1.1.1.1.1.1.1.1.1.2.1.2.1 depth=0 eapply trans_eq |
616 1.1.1.1.1.1.1.1.1.1.1.1.2.1.3 depth=0 eapply trans_eq | 616 1.1.1.1.1.1.1.1.1.1.1.1.2.1.3 depth=0 eapply trans_eq |
617 ]] | 617 ]] |