Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-02-07 04:25:55 -0800 (Mon, 07 Feb 2005)
Revision: 6624
Log message:
***************************************************************************
**** !!!!! WARNING !!!!! ****
***************************************************************************
!!!!! This commit breaks binary compatibility !!!!!
!!!!! Export all your uncommitted proofs before updating !!!!!
!!!!! !!!!!
!!!!! If you export to a .prla that did not exist before, you will !!!!!
!!!!! to edit it manually after you update - find the line that !!!!!
!!!!! starts with "NPerv!cons" replace the last (third) occurrence !!!!!
!!!!! of "cons" with "xcons", then replace last (third) occurrence !!!!!
!!!!! nil" with "xnil" on the "Perv!nil" line. !!!!!
!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
Merging the opname_classes branch!
This commit inroduces types to MetaPRL syntax with an informal (but pretty
precise) typechecking. Hopefully Jason will write some documentation
describing how to use this.
This fixes bug 370 and bug 371.