misc/misc2/reverse-by-separation.acl2
Added forms suggested by Camm Maguire to allow certification in GCL 2.6.8.

interface/emacs/acl2-interface.el
Made small modifications suggested by Camm Maguire, "in response to a
Debian bug regarding certain emacs policies."

Reflecting ACL2 system mods:

Quoting a comment put in books/system/doc/acl2-doc.lisp (deflabel xdoc
note-7-0 ...):

; Made a small GCL-only related change to user-homedir-pathname, after
; consultation with Camm Maguire.

Quoting :doc note-7-0:

  Modified code used in distributing Debian releases that allows books
  certified in one directory to be distributed in another. This
  change, together with the fact that such relocation is not truly
  supported, is explained in comments in source function
  make-certificate-file-relocated. Thanks to Camm Maguire for
  discussions leading to this change.


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

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2948 303c5b2c-9740-0410-b014-fd8f9db7be32
VL updates for more comprehensive parameter support

 - A new function, VL-CONSTEVAL, basically replaces VL-CONSTEXPR-REDUCE, and is
   generally much more sophisticated.  It can properly size and simplify many
   expressions that occur in lhs-free locations, such as array indices and
   parameter values.  The new function is used in the new unparameterization
   code (see below) and also in other transforms such as range/select
   resolution.

 - The syntax for parameter declarations and parameter arguments has been
   updated in order to support value parameters with arbitrary datatypes and
   type parameters.  This changes the VL-PARAMDECL-P representation and adds a
   new VL-PARAMARGS-P structure that is now used for the paramargs field of
   VL-MODINST-P.  It also involves updates to the parser, printer, and various
   transforms to support the new syntax.

 - The unparameterization transform is completely reworked and should now
   correctly support a much richer subset of SystemVerilog parameters.  New
   system tests have been added to try to ensure the new implementation is
   correctly processing many tricky cases.

Other VL changes

 - Made toe transform slightly more permissive so that it no longer complains
   about variable declarations.  This seems desirable for supporting "logic"
   types and occasionally helps with things like "output reg"...

 - Improved error message for toe-rejected constructs, e.g., it will now tell
   you which parameter/functions/tasks are still present.

 - Fix minor datatype pretty-printing bugs

 - Fix Verilog definitions of VL_1_BIT_BUFIF(0/1) to work around NCVerilog bug
   with optimizing ~~, similar to previous VL_1_BIT_BUF fix.

 - Removed mlib/sub-counts book, which wasn't really used for anything and
   was going to take some work to update for the new parameter code.

Miscellaneous changes:

 - Added FAL-FIND-ANY function to std/alists.

 - Fixed problem with error message in DEFINE.

git-svn-id: http://acl2-books.googlecode.com/svn/trunk@2949 303c5b2c-9740-0410-b014-fd8f9db7be32
Adding a wrapper for etags that allows for whitespace before the def-thingy (that's a technical term).

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