Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-09 03:31:26 -0700 (Wed, 09 Jul 2003)
Revision: 4726
Log message:

      Got rid of the "arg_subst" part of the tactic_arg - we never used it, and
      I do not thing it is likely to be useful in the future.
      

Changes	Path
+1 -16	metaprl/filter/boot/proof_term_boot.ml
+0 -1	metaprl/filter/boot/sequent_boot.ml
+0 -19	metaprl/filter/boot/tactic_boot.ml
+0 -7	metaprl/filter/boot/tactic_boot_sig.mlz
+0 -2	metaprl/filter/boot/tacticals_boot.ml
+0 -4	metaprl/support/display/summary.ml
+0 -2	metaprl/support/display/summary.mli
+0 -2	metaprl/support/shell/proof_edit.ml
+2 -2	metaprl/theories/experimental/compile/Makefile