patch ddc-head: SystemF2Data: working on type judgements

[Ben Lippmeier]

Mon Aug  1 08:50:05 EDT 2011  Ben Lippmeier <b...@ouroborus.net>
  * SystemF2Data: working on type judgements

    M ./proof/DDC/Language/SystemF2.v +9
    M ./proof/DDC/Language/SystemF2/Exp.v -4 +4
    M ./proof/DDC/Language/SystemF2/KiJudge.v -6 +5
    M ./proof/DDC/Language/SystemF2/SubstExpExp.v -1 +1
    M ./proof/DDC/Language/SystemF2/Ty.v -195 +3
    A ./proof/DDC/Language/SystemF2/TyBase.v
    M ./proof/DDC/Language/SystemF2/TyEnv.v -2 +2
    M ./proof/DDC/Language/SystemF2/TyJudge.v -4 +4
    A ./proof/DDC/Language/SystemF2/TyLift.v
    A ./proof/DDC/Language/SystemF2/TySubst.v
    M ./proof/DDC/Language/SystemF2Data/Def.v -32 +94
    M ./proof/DDC/Language/SystemF2Data/Exp.v -11 +12
    M ./proof/DDC/Language/SystemF2Data/ExpAlt.v -6 +6
    M ./proof/DDC/Language/SystemF2Data/ExpBase.v -5 +5
    M ./proof/DDC/Language/SystemF2Data/ExpLift.v -20 +49
    M ./proof/DDC/Language/SystemF2Data/ExpSubst.v -15 +40
    M ./proof/DDC/Language/SystemF2Data/TyJudge.v -29 +47

-- 
Disciple-Cafe mailing list
http://groups.google.com/group/disciple-cafe