Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2001-07-06 13:02:02 -0700 (Fri, 06 Jul 2001)
Revision: 3318
Log message:

      - Fixed some bugs in Itt_w:
        (a) The rule ruduce_tree_eta was unsound (we could prove unconditional
            eta from it). Removed
        (b) The rule wElimination was also unsound. Fixed.
        (c) There old bug noticed by Carl 2 years ago survived in the rule
            tree_indEquality. I fixed this rule, make it more general,
            make it interacative instead of primitive and proved it.
      
      - Display forms for srec and prec types are fixed.
      

Changes  Path
+1 -1 metaprl/theories/itt/Makefile
+6 -0 metaprl/theories/itt/itt_inv_typing.ml
+1 -1 metaprl/theories/itt/itt_prec.ml
+1 -1 metaprl/theories/itt/itt_srec.ml
+18 -15 metaprl/theories/itt/itt_w.ml
+3 -11 metaprl/theories/itt/itt_w.mli
Added metaprl/theories/itt/itt_w.prla
Properties metaprl/theories/itt/itt_w.prla