Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2004-10-12 01:45:01 -0700 (Tue, 12 Oct 2004)
Revision: 6238
Log message:

      Added all basic stuff for itt_reflection, including arities of bterms
      and elimination on bterms.
      
      In Base_reflection, a simple_bterm does not have to be a bterm.
      

Changes  Path
+8 -12 metaprl/theories/base/base_reflection.ml
+235 -49 metaprl/theories/itt/itt_reflection.ml
+13 -3 metaprl/theories/itt/itt_reflection.mli
+4145 -1294 metaprl/theories/itt/itt_reflection.prla
+0 -2 metaprl/theories/itt/itt_reflection_test.ml