some documentation fixes

diff --git a/INSTALL b/INSTALL
index 3008a576c941a42a89fedfd350b81272a5841665..f914f4fe9ba6bb7af1df9be050d104e6c9582d46 100644 (file)
--- 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 73865d1235c1b2a0b5580ed17884aea44da89666..d70d4c22110fd857a6dceea94c8dd896d81df11b 100644 (file)
--- 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 a5768c723f79af7ae410133310d0d735bcee8962..0ef6608bb463eb24a48748407d2518d80da78f66 100644 (file)
--- 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 07f964d463031c62890e193cc6b006950aa29189..488563b54606f29e1bbf0ab08d4ca11c748fe0d1 100644 (file)
--- 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