Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2005-12-24 17:32:38 -0800 (Sat, 24 Dec 2005)
Revision: 8359
Log message:

      Some simplifications.
      

Changes  Path
+12 -17 metaprl/theories/itt/core/itt_list2.ml
+30420 -21771 metaprl/theories/itt/core/itt_list2.prla
+0 -6 metaprl/theories/itt/extensions/vector/itt_vec_list1.ml
+2275 -2416 metaprl/theories/itt/extensions/vector/itt_vec_list1.prla
+459 -1899 metaprl/theories/itt/reflection/core/itt_hoas_vector.prla