Minor vl updates
  - Tweak vl model command to not print noisy serialize stats
  - Add explicit version tag to vl-design-p syntax
  - Clean up some noisy b* binders that weren't doing anything
  - Add another unparameterization systest
  - Add "make <testname>" capability to vl/systest/Makefile

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2951 303c5b2c-9740-0410-b014-fd8f9db7be32
Made a few documentation improvements, especially pertaining to the
cert_param feature for book certification (see :doc
books-certification).  Thanks to Jared and Sol for their help with
this.

oslib/ls.lisp: In consultation with Jared, restricted to CCL to avoid
an SBCL certification error for parent book oslib/tests/mkdir.lisp.


git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2952 303c5b2c-9740-0410-b014-fd8f9db7be32
deftypes: more aggressive theory management.  Fixes issue 214.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2953 303c5b2c-9740-0410-b014-fd8f9db7be32
deftypes: check for conflicts between field names and sum/product variable name (xvar).  Fixes issue 183.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2954 303c5b2c-9740-0410-b014-fd8f9db7be32