some documentation fixes

4 files changed, 39 insertions, 9 deletions

diff --git a/INSTALL b/INSTALL
index 3008a576c..f914f4fe9 100644
--- a/INSTALL
+++ b/INSTALL
@@ -1,4 +1,4 @@
-This is CVC4 release version 1.0.
+ is CVC4 release version 1.0.
 
 *** Quick-start instructions
 
@@ -22,7 +22,8 @@ system tests and regression tests should pass without incident.
 To build API documentation, use "make doc".  Documentation is produced
 under doc/ but is not installed by "make install".
 
-Examples/tutorials are not installed with "make install."  See below.
+Examples and tutorials are not installed with "make install."  See
+below.
 
 For more information about the build system itself (probably not
 necessary for casual users), see the Appendix at the bottom of this
@@ -121,7 +122,7 @@ Boost base library) is needed to run CVC4 in "portfolio"
 CxxTest is necessary to run CVC4's unit tests (included with the
 distribution).  Running these is not really required for users of
 CVC4; "make check" will skip unit tests if CxxTest isn't available,
-and go on to run the extensive system- and regresion-tests in the
+and go on to run the extensive system- and regression-tests in the
 source tree.  However, if you're interested, you can download CxxTest
 at http://cxxtest.com/ .
 
@@ -153,6 +154,10 @@ here (along with the CVC4 Debian packages):
 
   deb http://cvc4.cs.nyu.edu/debian/ unstable/
 
+On Debian (and Debian-derived distributions like Ubuntu), you only
+need to drop that one line in your /etc/apt/sources.list file, and
+then install with your favorite package manager.
+
 The Debian source package "cudd", available from the same repository,
 includes a diff of all changes made to cudd makefiles.
 
@@ -210,11 +215,11 @@ source tarball.
 
 First, use "./autogen.sh" to create the configure script.  Then
 proceed as normal for any distribution tarball.  The parsers are
-pre-generated for the tarballs; hence the extra ANTLR3 requirement to
-generate the source code for the parsers, when building from the
-repository.
+pre-generated for the tarballs, but don't exist in the repository;
+hence the extra ANTLR3 requirement to generate the source code for the
+parsers, when building from the repository.
 
-*** Examples/tutorials are not built or installed
+*** Examples and tutorials are not built or installed
 
 Examples are not built by "make" or "make install".  See
 examples/README for information on what to find in the examples/
diff --git a/README b/README
index 73865d123..d70d4c221 100644
--- a/README
+++ b/README
@@ -32,6 +32,31 @@ We recommend that you visit our CVC4 tutorials online at:
 
 for help getting started using CVC4.
 
+*** Contributing to the CVC4 project
+
+We are always happy to hear feedback from our users:
+
+* if you need help with using CVC4, please write to the
+  cvc-users@cs.nyu.edu mailing list.
+
+* if you need to report a bug with CVC4, or make a feature request,
+  please visit our bugtracker at http://cvc4.cs.nyu.edu/bugs/ or write
+  to the cvc-bugs@cs.nyu.edu mailing list.  We are very grateful for
+  bug reports, as they help us improve CVC4, and patches are generally
+  reviewed and accepted quickly.
+
+* if you are using CVC4 in your work, or incorporating it into
+  software of your own, we'd like to invite you to leave a description
+  and link to your project/software on our "Third Party Applications"
+  page at http://cvc4.cs.nyu.edu/wiki/Public:Third_Party_Applications
+
+* if you are interested in contributing code (for example, a new
+  decision procedure implementation) to the CVC4 project, please
+  contact us at cvc4-devel@cs.nyu.edu.  We'd be happy to point you to
+  some internals documentation to help you out.
+
+Thank you for using CVC4!
+
 *** The History of CVC4
 
 The Cooperating Validity Checker series has a long history.  The
diff --git a/src/util/util_model.cpp b/src/util/util_model.cpp
index a5768c723..0ef6608bb 100644
--- a/src/util/util_model.cpp
+++ b/src/util/util_model.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file model.cpp
+/*! \file util_model.cpp
  ** \verbatim
  ** Original author: ajreynol
  ** Major contributors: mdeters
diff --git a/src/util/util_model.h b/src/util/util_model.h
index 07f964d46..488563b54 100644
--- a/src/util/util_model.h
+++ b/src/util/util_model.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file model.h
+/*! \file util_model.h
  ** \verbatim
  ** Original author: ajreynol
  ** Major contributors: mdeters