Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-04-28 23:03:39 -0700 (Mon, 28 Apr 2003)
Revision: 4511
Log message:

      Made the tactic type completely abstract. From now on, use funT (and argfunT)
      for writing tactics that need to look up information from tactic_arg.
      

Changes  Path
+3 -3 metaprl/filter/boot/conversionals_boot.ml
+27 -30 metaprl/filter/boot/rewrite_boot.ml
+0 -1 metaprl/filter/boot/sequent_boot.ml
+0 -1 metaprl/filter/boot/sequent_boot.mli
+19 -3 metaprl/filter/boot/tactic_boot.ml
+0 -2 metaprl/filter/boot/tactic_boot.mli
+12 -13 metaprl/filter/boot/tactic_boot_sig.mlz
+0 -2 metaprl/filter/boot/tactic_type.mli
+127 -144 metaprl/filter/boot/tacticals_boot.ml
+0 -1 metaprl/filter/boot/tacticals_boot.mli
+4 -4 metaprl/filter/filter/filter_prog.ml
+17 -20 metaprl/theories/base/base_auto_tactic.ml
+30 -31 metaprl/theories/base/base_dtactic.ml
+12 -12 metaprl/theories/czf/czf_itt_eq.ml
+8 -8 metaprl/theories/czf/czf_itt_equiv.ml
+4 -8 metaprl/theories/czf/czf_itt_group.ml
+2 -4 metaprl/theories/czf/czf_itt_hom.ml
+4 -8 metaprl/theories/czf/czf_itt_ker.ml
+3 -2 metaprl/theories/czf/czf_itt_nat.ml
+1 -2 metaprl/theories/czf/czf_itt_normal_subgroup.ml
+3 -2 metaprl/theories/czf/czf_itt_power.ml
+1 -1 metaprl/theories/czf/czf_itt_power.mli
+12 -13 metaprl/theories/czf/czf_itt_set.ml
+9 -8 metaprl/theories/czf/czf_itt_set_ind.ml
+4 -3 metaprl/theories/fol/cfol_itt_base.ml
+22 -24 metaprl/theories/fol/fol_prop.ml
+4 -6 metaprl/theories/fol/fol_struct.ml
+9 -12 metaprl/theories/itt/itt_bisect.ml
+7 -7 metaprl/theories/itt/itt_bool.ml
+4 -4 metaprl/theories/itt/itt_collection.ml
+8 -8 metaprl/theories/itt/itt_derive.ml
+10 -13 metaprl/theories/itt/itt_disect.ml
+2 -2 metaprl/theories/itt/itt_dprod.ml
+14 -13 metaprl/theories/itt/itt_equal.ml
+8 -8 metaprl/theories/itt/itt_fset.ml
+17 -18 metaprl/theories/itt/itt_fun.ml
+71 -89 metaprl/theories/itt/itt_int_arith.ml
+4 -4 metaprl/theories/itt/itt_int_base.ml
+10 -10 metaprl/theories/itt/itt_isect.ml
+50 -50 metaprl/theories/itt/itt_logic.ml
+2 -2 metaprl/theories/itt/itt_nat.ml
+14 -16 metaprl/theories/itt/itt_prop_decide.ml
+3 -3 metaprl/theories/itt/itt_quotient.ml
+28 -48 metaprl/theories/itt/itt_record.ml
+2 -2 metaprl/theories/itt/itt_relation_str.ml
+4 -4 metaprl/theories/itt/itt_sort.ml
+33 -42 metaprl/theories/itt/itt_squash.ml
+4 -4 metaprl/theories/itt/itt_squiggle.ml
+28 -33 metaprl/theories/itt/itt_struct.ml
+16 -22 metaprl/theories/itt/itt_struct2.ml
+5 -5 metaprl/theories/itt/itt_struct3.ml
+13 -13 metaprl/theories/itt/itt_subtype.ml
+6 -7 metaprl/theories/sil/sil_itt_sos.ml
+18 -4 metaprl/theories/tactic/top_tacticals.ml
+7 -10 metaprl/theories/tptp/tptp.ml
+56 -55 metaprl/theories/tptp/tptp_prove.ml