Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-08 15:14:42 -0700 (Thu, 08 Aug 2002)
Revision: 3778
Log message:

      Flushing out some work on the typing rules.
      
      I've added kinds and some judgments to mfir_sequent.  For mfir_ty, I've had to
      change how some types are represented (so that we get a convinient binding
      structure), and I've also added terms to represent some typing definitions.
      Added some typing rules, which I think all work as expected now.  Comments and
      documentation might need some clarifying still, but at least something's there
      for now.
      

Changes  Path
+1 -0 metaprl/theories/fir/README
+18 -2 metaprl/theories/fir/mfir_basic.ml
+29 -23 metaprl/theories/fir/mfir_basic.mli
+3 -3 metaprl/theories/fir/mfir_exp.ml
+138 -15 metaprl/theories/fir/mfir_sequent.ml
+27 -2 metaprl/theories/fir/mfir_sequent.mli
+32 -9 metaprl/theories/fir/mfir_termOp.ml
+22 -4 metaprl/theories/fir/mfir_termOp.mli
+3 -0 metaprl/theories/fir/mfir_termOp_base.ml
+3 -0 metaprl/theories/fir/mfir_termOp_base.mli
+0 -11 metaprl/theories/fir/mfir_test.ml
+63 -22 metaprl/theories/fir/mfir_ty.ml
+10 -3 metaprl/theories/fir/mfir_ty.mli
+122 -8 metaprl/theories/fir/mfir_type_rules.ml