comparison src/Large.v @ 437:8077352044b2

A pass over all formatting, after big pile of coqdoc changes
author Adam Chlipala <adam@chlipala.net>
date Fri, 27 Jul 2012 16:47:28 -0400
parents a54a4a2ea6e4
children 0650420c127b
comparison
equal deleted inserted replaced
436:5d5e44f905c7 437:8077352044b2
461 461
462 Undo. 462 Undo.
463 info t. 463 info t.
464 464
465 (* begin hide *) 465 (* begin hide *)
466 (* begin thide *)
466 Definition eir := eq_ind_r. 467 Definition eir := eq_ind_r.
468 (* end thide *)
467 (* end hide *) 469 (* end hide *)
468 470
469 (** %\vspace{-.15in}%[[ 471 (** %\vspace{-.15in}%[[
470 == simpl in *; intuition; subst; autorewrite with core in *; 472 == simpl in *; intuition; subst; autorewrite with core in *;
471 simpl in *; intuition; subst; autorewrite with core in *; 473 simpl in *; intuition; subst; autorewrite with core in *;
589 591
590 Restart. 592 Restart.
591 debug eauto 6. 593 debug eauto 6.
592 594
593 (* begin hide *) 595 (* begin hide *)
596 (* begin thide *)
594 Definition deeeebug := (@eq_refl, @sym_eq). 597 Definition deeeebug := (@eq_refl, @sym_eq).
598 (* end thide *)
595 (* end hide *) 599 (* end hide *)
596 600
597 (** The output is a large proof tree. The beginning of the tree is enough to reveal what is happening: 601 (** The output is a large proof tree. The beginning of the tree is enough to reveal what is happening:
598 [[ 602 [[
599 1 depth=6 603 1 depth=6
753 757
754 758
755 (** * Build Processes *) 759 (** * Build Processes *)
756 760
757 (* begin hide *) 761 (* begin hide *)
762 (* begin thide *)
758 Module Lib. 763 Module Lib.
759 Module A. 764 Module A.
760 End A. 765 End A.
761 Module B. 766 Module B.
762 End B. 767 End B.
767 Module D. 772 Module D.
768 End D. 773 End D.
769 Module E. 774 Module E.
770 End E. 775 End E.
771 End Client. 776 End Client.
777 (* end thide *)
772 (* end hide *) 778 (* end hide *)
773 779
774 (** As in software development, large Coq projects are much more manageable when split across multiple files and when decomposed into libraries. Coq and Proof General provide very good support for these activities. 780 (** As in software development, large Coq projects are much more manageable when split across multiple files and when decomposed into libraries. Coq and Proof General provide very good support for these activities.
775 781
776 Consider a library that we will name [Lib], housed in directory <<LIB>> and split between files <<A.v>>, <<B.v>>, and <<C.v>>. A simple %\index{Makefile}%Makefile will compile the library, relying on the standard Coq tool %\index{coq\_makefile}%<<coq_makefile>> to do the hard work. 782 Consider a library that we will name [Lib], housed in directory <<LIB>> and split between files <<A.v>>, <<B.v>>, and <<C.v>>. A simple %\index{Makefile}%Makefile will compile the library, relying on the standard Coq tool %\index{coq\_makefile}%<<coq_makefile>> to do the hard work.