Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-05-28 06:48:44 -0700 (Thu, 28 May 1998)
Revision: 2190
Log message:

      Updated the editor to use new Refiner structure.
      ITT needs dform names.
      

Changes	Path
+4 -0	metaprl/Makefile
Properties	metaprl/editor/ml
+3 -0	metaprl/editor/ml/Makefile
Added	metaprl/editor/ml/io_proof.ml
Properties	metaprl/editor/ml/io_proof.ml
Added	metaprl/editor/ml/io_proof.mli
Properties	metaprl/editor/ml/io_proof.mli
Added	metaprl/editor/ml/io_proof_type.mlz
Properties	metaprl/editor/ml/io_proof_type.mlz
+10 -4	metaprl/editor/ml/package_df.ml
+7 -3	metaprl/editor/ml/package_df.mli
+337 -36	metaprl/editor/ml/package_info.ml
+16 -1	metaprl/editor/ml/package_info.mli
+21 -3	metaprl/editor/ml/package_type.mlz
+41 -35	metaprl/editor/ml/proof.ml
+10 -6	metaprl/editor/ml/proof.mli
+13 -4	metaprl/editor/ml/proof_edit.ml
+8 -4	metaprl/editor/ml/proof_edit.mli
+20 -15	metaprl/editor/ml/proof_step.ml
+10 -6	metaprl/editor/ml/proof_step.mli
+9 -7	metaprl/editor/ml/shell.ml
+5 -1	metaprl/editor/ml/shell.mli
+5 -1	metaprl/editor/ml/shell_null.ml
+6 -1	metaprl/editor/ml/shell_p4.ml
+5 -1	metaprl/editor/ml/shell_p4.mli
+118 -67	metaprl/editor/ml/shell_rewrite.ml
+12 -13	metaprl/editor/ml/shell_rewrite.mli
+7 -3	metaprl/editor/ml/shell_type.mlz
Properties	metaprl/filter
+0 -2	metaprl/filter/Makefile
+10 -6	metaprl/filter/filter_bin.ml
+22 -22	metaprl/filter/filter_cache.ml
+11 -6	metaprl/filter/filter_cache.mli
+10 -1	metaprl/filter/filter_cache_fun.ml
+7 -3	metaprl/filter/filter_parse.ml
+79 -26	metaprl/filter/filter_prog.ml
+12 -3	metaprl/filter/filter_prog.mli
Deleted	metaprl/filter/filter_proof.ml
Deleted	metaprl/filter/filter_proof.mli
Deleted	metaprl/filter/filter_proof_type.mlz
+20 -16	metaprl/filter/filter_summary.ml
+5 -1	metaprl/filter/filter_summary.mli
+5 -0	metaprl/library/ascii_scan.ml
+5 -0	metaprl/library/basic.ml
+5 -0	metaprl/library/bigInt.ml
+5 -0	metaprl/library/db.ml
+5 -0	metaprl/library/definition.ml
+5 -0	metaprl/library/int32.ml
+5 -0	metaprl/library/library.ml
+3 -0	metaprl/library/library_eval.ml
+9 -0	metaprl/library/library_type_base.ml
+5 -0	metaprl/library/link.ml
+5 -0	metaprl/library/mathBus.ml
+6 -2	metaprl/library/mbterm.ml
+5 -0	metaprl/library/nuprl5.ml
+5 -0	metaprl/library/object_id.ml
+5 -0	metaprl/library/oidtable.ml
+5 -0	metaprl/library/orb.ml
+7 -0	metaprl/library/registry.ml
+5 -0	metaprl/library/socketIo.ml
+5 -0	metaprl/library/tentfunctor.ml
+7 -2	metaprl/library/test.ml
+5 -0	metaprl/library/utils.ml
+3 -3	metaprl/mk/config
+2 -2	metaprl/refiner/Makefile
+8 -4	metaprl/theories/base/base_cache.ml
+8 -4	metaprl/theories/base/base_cache.mli
+7 -1	metaprl/theories/base/base_dform.ml
+32 -28	metaprl/theories/base/base_dtactic.ml
+5 -1	metaprl/theories/base/base_dtactic.mli
+4 -1	metaprl/theories/base/evaluator.ml
+1 -1	metaprl/theories/base/evaluator.mli
+30 -26	metaprl/theories/base/typeinf.ml
+14 -10	metaprl/theories/base/typeinf.mli
+1 -1	metaprl/theories/itt/Makefile
+5 -1	metaprl/theories/itt/itt_atom.ml
+5 -1	metaprl/theories/itt/itt_atom.mli
+5 -1	metaprl/theories/itt/itt_dfun.ml
+5 -1	metaprl/theories/itt/itt_dfun.mli
+5 -1	metaprl/theories/itt/itt_dprod.ml
+5 -1	metaprl/theories/itt/itt_dprod.mli
+5 -1	metaprl/theories/itt/itt_equal.ml
+5 -1	metaprl/theories/itt/itt_equal.mli
+5 -1	metaprl/theories/itt/itt_ext_equal.ml
+5 -1	metaprl/theories/itt/itt_ext_equal.mli
+5 -1	metaprl/theories/itt/itt_fun.ml
+5 -1	metaprl/theories/itt/itt_int.ml
+5 -1	metaprl/theories/itt/itt_int.mli
+5 -1	metaprl/theories/itt/itt_isect.ml
+5 -1	metaprl/theories/itt/itt_isect.mli
+5 -1	metaprl/theories/itt/itt_list.ml
+5 -1	metaprl/theories/itt/itt_list.mli
+5 -1	metaprl/theories/itt/itt_logic.ml
+5 -1	metaprl/theories/itt/itt_logic.mli
+5 -1	metaprl/theories/itt/itt_prec.ml
+5 -1	metaprl/theories/itt/itt_prec.mli
+5 -1	metaprl/theories/itt/itt_prod.ml
+5 -1	metaprl/theories/itt/itt_quotient.ml
+5 -1	metaprl/theories/itt/itt_quotient.mli
+1 -1	metaprl/theories/itt/itt_redrules.ml
+5 -1	metaprl/theories/itt/itt_rfun.ml
+5 -1	metaprl/theories/itt/itt_rfun.mli
+5 -1	metaprl/theories/itt/itt_set.ml
+5 -1	metaprl/theories/itt/itt_set.mli
+5 -1	metaprl/theories/itt/itt_soft.ml
+5 -1	metaprl/theories/itt/itt_soft.mli
+21 -17	metaprl/theories/itt/itt_squash.ml
+5 -1	metaprl/theories/itt/itt_squash.mli
+5 -1	metaprl/theories/itt/itt_srec.ml
+5 -1	metaprl/theories/itt/itt_srec.mli
+5 -1	metaprl/theories/itt/itt_struct.ml
+5 -1	metaprl/theories/itt/itt_struct.mli
+5 -1	metaprl/theories/itt/itt_subtype.ml
+5 -1	metaprl/theories/itt/itt_subtype.mli
+5 -1	metaprl/theories/itt/itt_union.ml
+5 -1	metaprl/theories/itt/itt_union.mli
+5 -1	metaprl/theories/itt/itt_unit.ml
+5 -1	metaprl/theories/itt/itt_unit.mli
+5 -1	metaprl/theories/itt/itt_void.ml
+5 -1	metaprl/theories/itt/itt_void.mli
+5 -0	metaprl/theories/ocaml/ocaml_base_df.ml
+5 -0	metaprl/theories/ocaml/perv.ml
+5 -1	metaprl/theories/rewrite/rw_beta.ml
+5 -1	metaprl/theories/tactic/options.ml
+35 -29	metaprl/theories/tactic/sequent.ml
+5 -1	metaprl/theories/tactic/sequent.mli
+7 -2	metaprl/theories/tactic/tactic_cache.ml
+5 -1	metaprl/theories/tactic/tactic_cache.mli
+23 -8	metaprl/theories/tactic/tactic_type.mlz
+14 -9	metaprl/theories/tactic/tacticals.ml
+5 -1	metaprl/theories/tactic/tacticals.mli
+1 -0	metaprl/util/Makefile