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 ]]