Merging from ragedl/acl2

I'll handle the pull request myself, so nothing for anyone else to do.