Comp-gcl
Compile some ACL2 functions leaving .c and .h files
Comp-gcl is for use by experts who want to examine the results
of GCL compilation, and it may only be used with ACL2 implementations built on
top of GCL. It takes exactly the same arguments as comp, and has the
same basic functionality (see comp), but has two additional effects.
First, files "TMP.lisp" and "TMP1.lisp" are always created, even
when a single function is specified. Second, comp-gcl always leaves
files "TMP.c", "TMP.h", "TMP1.c", and "TMP1.h"
when compilation is complete.
