Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-03-21 20:40:59 -0800 (Mon, 21 Mar 2005)
Revision: 6994
Log message:

      - Iforms now do not have to be duplicated in .mli and .ml - iforms that exist
        in .mli, but not in .ml will now be automatically copied to .ml.
      
      - No ML code is generated for iforms now; since filter_grammar handles
        iforms internally, there is no need for explicit ML code.
      
      - The .cmoz/.cmiz data structure for iforms now contains neither proofs nor
        resources (note - MetaPRL should still be able to read older binaries).
      
      - Removed references to arguments and conditions from the code for iforms,
        since iforms can not be conditional and can not take arguments.
      

Changes  Path
+1 -1 metaprl/OMakefile
+2 -2 metaprl/filter/base/filter_cache_fun.ml
+7 -4 metaprl/filter/base/filter_magic.ml
+104 -83 metaprl/filter/base/filter_summary.ml
+1 -1 metaprl/filter/base/filter_summary_type.ml
+8 -3 metaprl/filter/base/filter_type.ml
+22 -35 metaprl/filter/filter/filter_parse.ml
+5 -18 metaprl/filter/filter/filter_prog.ml
+6 -9 metaprl/filter/filter/term_grammar.ml
+2 -2 metaprl/refiner/refiner/refine.ml
+4 -6 metaprl/refiner/refiner/refiner_debug.ml
+2 -3 metaprl/refiner/reflib/term_ty_infer.ml
+1 -1 metaprl/refiner/reflib/term_ty_infer.mli
+0 -3 metaprl/refiner/refsig/refine_sig.ml
+3 -6 metaprl/support/display/summary.ml
+2 -2 metaprl/support/shell/package_info.ml
+3 -3 metaprl/support/shell/shell_state.ml
+0 -0 metaprl/theories/itt/itt_list2.ml
+3 -3 metaprl/theories/itt/itt_list2.prla
+0 -2 metaprl/theories/itt/itt_synt_operator.ml
+0 -2 metaprl/theories/itt/itt_synt_var.ml