Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-18 21:29:12 -0700 (Fri, 18 Apr 2003)
Revision: 4456
Log message:

      - Moved Filter_prog from filter/base to filter/filter and removed it
      from the list of modules being linked into the editor/ml/mp.* binaries.
      
      - Also, simplified some of the signatures (replacing functors with plain modules)
      
      Note: we might want to be eventually able to define things on-line from the toploop
      and filter_prog might be useful to have linked in for that purpose. But currently
      filter_parse is in filter/filter (and not being linked in anyway), so this change
      does not make things any worse than they already were.
      

Changes  Path
+1 -1 metaprl/editor/ml/package_sig.mlz
+4 -4 metaprl/editor/ml/proof_edit.ml
+1 -1 metaprl/editor/ml/proof_edit.mli
+4 -4 metaprl/editor/ml/shell.ml
+1 -1 metaprl/editor/ml/shell_package.ml
+1 -1 metaprl/editor/ml/shell_rewrite.ml
+1 -1 metaprl/editor/ml/shell_rewrite.mli
+1 -1 metaprl/editor/ml/shell_rule.ml
+1 -1 metaprl/editor/ml/shell_rule.mli
+2 -0 metaprl/filter/Makefile
+0 -1 metaprl/filter/base/Files
+4 -33 metaprl/filter/base/filter_cache.ml
+3 -68 metaprl/filter/base/filter_cache.mli
Deleted metaprl/filter/base/filter_prog.ml
Deleted metaprl/filter/base/filter_prog.mli
+69 -2 metaprl/filter/base/filter_summary_type.ml
+2 -2 metaprl/filter/boot/proof_convert.mli
+1 -0 metaprl/filter/filter/Files
+5 -16 metaprl/filter/filter/filter_bin.ml
+4 -11 metaprl/filter/filter/filter_convert.ml
+5 -16 metaprl/filter/filter/filter_parse.ml
Added metaprl/filter/filter/filter_prog.ml
Properties metaprl/filter/filter/filter_prog.ml
Added metaprl/filter/filter/filter_prog.mli
Properties metaprl/filter/filter/filter_prog.mli