Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1999-04-04 15:07:38 -0700 (Sun, 04 Apr 1999)
Revision: 2629
Log message:

      This is the first phase for modifying resources.
      The Mp_resource interface has been substantially simplified, but
      I believe that it retains as much functionality as it did before
      the change.
      
      The next step for me to add the Mp_resource support for
      adding resources as rule annotations.
      

Changes  Path
+10 -10 metaprl/editor/ml/package_info.ml
+4 -4 metaprl/editor/ml/shell_mp.ml
+2 -0 metaprl/filter/filter_comment.ml
+10 -0 metaprl/filter/filter_hash.ml
+36 -0 metaprl/filter/filter_ocaml.ml
+10 -10 metaprl/filter/filter_prog.ml
+10 -0 metaprl/filter/mLast_util.ml
+1 -1 metaprl/mk/rules
+90 -10 metaprl/refiner/reflib/mp_resource.ml
+45 -11 metaprl/refiner/reflib/mp_resource.mli
+32 -93 metaprl/theories/base/base_auto_tactic.ml
+4 -4 metaprl/theories/base/base_auto_tactic.mli
+18 -47 metaprl/theories/base/base_cache.ml
+4 -7 metaprl/theories/base/base_cache.mli
+16 -44 metaprl/theories/base/base_dtactic.ml
+5 -5 metaprl/theories/base/base_rewrite.ml
+28 -84 metaprl/theories/base/typeinf.ml
+4 -4 metaprl/theories/czf/czf_itt_all.ml
+4 -4 metaprl/theories/czf/czf_itt_and.ml
+3 -3 metaprl/theories/czf/czf_itt_dall.ml
+3 -3 metaprl/theories/czf/czf_itt_dexists.ml
+2 -2 metaprl/theories/czf/czf_itt_empty.ml
+11 -11 metaprl/theories/czf/czf_itt_eq.ml
+4 -4 metaprl/theories/czf/czf_itt_eq_inner.ml
+4 -4 metaprl/theories/czf/czf_itt_exists.ml
+4 -4 metaprl/theories/czf/czf_itt_false.ml
+6 -6 metaprl/theories/czf/czf_itt_implies.ml
+2 -2 metaprl/theories/czf/czf_itt_member.ml
+4 -4 metaprl/theories/czf/czf_itt_or.ml
+7 -7 metaprl/theories/czf/czf_itt_pre_set.ml
+1 -1 metaprl/theories/czf/czf_itt_rel.ml
+2 -2 metaprl/theories/czf/czf_itt_sall.ml
+2 -2 metaprl/theories/czf/czf_itt_sep.ml
+8 -8 metaprl/theories/czf/czf_itt_set.ml
+7 -7 metaprl/theories/czf/czf_itt_set_ext.ml
+4 -4 metaprl/theories/czf/czf_itt_set_ind.ml
+2 -2 metaprl/theories/czf/czf_itt_sexists.ml
+10 -10 metaprl/theories/czf/czf_itt_small.ml
+4 -4 metaprl/theories/czf/czf_itt_true.ml
+2 -2 metaprl/theories/czf/czf_itt_union.ml
+2 -2 metaprl/theories/fol/fol_all.ml
+2 -2 metaprl/theories/fol/fol_and.ml
+2 -2 metaprl/theories/fol/fol_bisect_itt.ml
+2 -2 metaprl/theories/fol/fol_exists.ml
+2 -2 metaprl/theories/fol/fol_false.ml
+2 -2 metaprl/theories/fol/fol_implies.ml
+2 -2 metaprl/theories/fol/fol_not.ml
+2 -2 metaprl/theories/fol/fol_or.ml
+1 -1 metaprl/theories/fol/fol_struct.ml
+2 -2 metaprl/theories/fol/fol_true.ml
+1 -1 metaprl/theories/fol/fol_type.ml
+1 -1 metaprl/theories/fol/fol_univ.ml
+3 -3 metaprl/theories/fol/fol_univ_itt.ml
+7 -7 metaprl/theories/itt/itt_atom.ml
+2 -2 metaprl/theories/itt/itt_atom_bool.ml
+7 -7 metaprl/theories/itt/itt_bisect.ml
+26 -26 metaprl/theories/itt/itt_bool.ml
+4 -4 metaprl/theories/itt/itt_bunion.ml
+10 -10 metaprl/theories/itt/itt_dfun.ml
+11 -11 metaprl/theories/itt/itt_dprod.ml
+28 -54 metaprl/theories/itt/itt_equal.ml
+9 -9 metaprl/theories/itt/itt_fset.ml
+11 -11 metaprl/theories/itt/itt_fun.ml
+7 -7 metaprl/theories/itt/itt_int.ml
+2 -2 metaprl/theories/itt/itt_int_bool.ml
+8 -8 metaprl/theories/itt/itt_isect.ml
+19 -19 metaprl/theories/itt/itt_list.ml
+5 -5 metaprl/theories/itt/itt_list2.ml
+53 -53 metaprl/theories/itt/itt_logic.ml
+2 -2 metaprl/theories/itt/itt_prec.ml
+8 -8 metaprl/theories/itt/itt_prod.ml
+8 -8 metaprl/theories/itt/itt_quotient.ml
+5 -5 metaprl/theories/itt/itt_rfun.ml
+8 -9 metaprl/theories/itt/itt_set.ml
+18 -45 metaprl/theories/itt/itt_squash.ml
+4 -4 metaprl/theories/itt/itt_squash.mli
+6 -6 metaprl/theories/itt/itt_srec.ml
+1 -1 metaprl/theories/itt/itt_struct.ml
+19 -47 metaprl/theories/itt/itt_subtype.ml
+4 -4 metaprl/theories/itt/itt_tsub.ml
+5 -5 metaprl/theories/itt/itt_tunion.ml
+14 -14 metaprl/theories/itt/itt_union.ml
+10 -11 metaprl/theories/itt/itt_unit.ml
+7 -9 metaprl/theories/itt/itt_void.ml
+11 -11 metaprl/theories/itt/itt_w.ml
+10 -10 metaprl/theories/reflect_itt/refl_raw_term.ml
+1 -1 metaprl/theories/reflect_itt/refl_term.ml
+3 -3 metaprl/theories/reflect_itt/refl_var.ml
+15 -42 metaprl/theories/tactic/conversionals.ml
+1 -1 metaprl/theories/tactic/conversionals.mli
+22 -65 metaprl/theories/tactic/mptop.ml
+4 -8 metaprl/theories/tactic/mptop.mli
Added metaprl/theories/tactic/pre_tactic_type.ml
Properties metaprl/theories/tactic/pre_tactic_type.ml
Added metaprl/theories/tactic/pre_tactic_type.mli
Properties metaprl/theories/tactic/pre_tactic_type.mli
+7 -7 metaprl/theories/tptp/tptp.ml