Cert.pl: call make with all-cert-pl-certs as targets, rather than the list of targets, which could overflow the shell ARG_MAX
flag.lisp: improvements to def-doublevar-induction
VL: add (tentative) support for function calls in sizing
fty: add maybe-natp as a basetype
     verify guards by default for equivalences introduced by deffixtype
Merge
merge
merge
Tweaked :short sections for :doc fmt etc. following suggestion from David Rager.  Updated manual distribution script to allow for search, by adding commands from David, as he requested.  Tweaked defpm utility to add useful "-COMMUTED" rule.

Note: Sol and I are debugging an issue that might cause a regression
failure, but probably not (my failure was probably due to the need for
a "clean", and we're looking into why that might be).