Mercurial > cpdt > repo
diff 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 |
line wrap: on
line diff
--- a/src/Large.v Fri Jul 27 15:41:06 2012 -0400 +++ b/src/Large.v Fri Jul 27 16:47:28 2012 -0400 @@ -463,7 +463,9 @@ info t. (* begin hide *) + (* begin thide *) Definition eir := eq_ind_r. + (* end thide *) (* end hide *) (** %\vspace{-.15in}%[[ @@ -591,7 +593,9 @@ debug eauto 6. (* begin hide *) + (* begin thide *) Definition deeeebug := (@eq_refl, @sym_eq). + (* end thide *) (* end hide *) (** The output is a large proof tree. The beginning of the tree is enough to reveal what is happening: @@ -755,6 +759,7 @@ (** * Build Processes *) (* begin hide *) +(* begin thide *) Module Lib. Module A. End A. @@ -769,6 +774,7 @@ Module E. End E. End Client. +(* end thide *) (* end hide *) (** 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.