Changes by: Brian Emre Aydemir (baydemir at cis.upenn.edu)
Date: 2002-08-06 14:00:47 -0700 (Tue, 06 Aug 2002)
Revision: 3773
Log message:

      Removed mfir_comment since it was redundant; the functionality it provided was
      already present elsewhere in MetaPRL.  Cleaned up Mfir_basic, Mfir_ty, and
      Mfir_exp as needed as a result of this.
      
      Added some additional support for integers and booleans to Mfir_basic so that
      I can start playing around with typing rules.  The Mfir_sequent module will
      deal with, you guessed it, sequent related items.  The Mfir_type_rules file
      will contain the typing rules (at least for now).
      
      The Mfir_test module will be used to test small examples, or to perform
      ``sanity checks'' on other aspects of the theory.
      

Changes  Path
+5 -3 metaprl/theories/fir/Makefile
+3 -1 metaprl/theories/fir/README
+322 -8 metaprl/theories/fir/mfir_basic.ml
+64 -8 metaprl/theories/fir/mfir_basic.mli
Deleted metaprl/theories/fir/mfir_comment.ml
Deleted metaprl/theories/fir/mfir_comment.mli
+38 -39 metaprl/theories/fir/mfir_exp.ml
+5 -8 metaprl/theories/fir/mfir_exp.mli
Added metaprl/theories/fir/mfir_sequent.ml
Properties metaprl/theories/fir/mfir_sequent.ml
Added metaprl/theories/fir/mfir_sequent.mli
Properties metaprl/theories/fir/mfir_sequent.mli
+126 -43 metaprl/theories/fir/mfir_termOp.ml
+92 -26 metaprl/theories/fir/mfir_termOp.mli
Added metaprl/theories/fir/mfir_test.ml
Properties metaprl/theories/fir/mfir_test.ml
Added metaprl/theories/fir/mfir_test.mli
Properties metaprl/theories/fir/mfir_test.mli
+3 -2 metaprl/theories/fir/mfir_theory.mlz
+7 -10 metaprl/theories/fir/mfir_ty.ml
+2 -6 metaprl/theories/fir/mfir_ty.mli
Added metaprl/theories/fir/mfir_type_rules.ml
Properties metaprl/theories/fir/mfir_type_rules.ml
Added metaprl/theories/fir/mfir_type_rules.mli
Properties metaprl/theories/fir/mfir_type_rules.mli