Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2004-06-24 05:27:02 -0700 (Thu, 24 Jun 2004)
Revision: 6010
Log message:

      This implements the bug 169 RFE - now one can finally just say "open Basic_tactics"
      and not worry about having to open all kinds of Refiner.*, Tactic_type.*, Top_*,
      etc!
      
      Note that the new support/tactics/basic_tactcs.ml file does not have an .mli
      and would not currently compile under make.
      

Changes  Path
+1 -1 metaprl/editor/ml/tests/prop-pigeon.mli
+2 -2 metaprl/filter/filter/filter_prog.ml
+2 -2 metaprl/filter/phobos/phobos_rewrite.ml
+1 -1 metaprl/filter/phobos/phobos_rewrite.mli
+1 -1 metaprl/support/shell/proof_edit.ml
+1 -1 metaprl/support/shell/proof_edit.mli
+1 -1 metaprl/support/shell/shell_core.mli
+2 -1 metaprl/support/tactics/OMakefile
+1 -0 metaprl/support/tactics/auto_tactic.ml
+1 -1 metaprl/support/tactics/base_cache.ml
+1 -1 metaprl/support/tactics/base_cache.mli
Added metaprl/support/tactics/basic_tactics.ml
Properties metaprl/support/tactics/basic_tactics.ml
+1 -0 metaprl/support/tactics/dtactic.ml
+1 -1 metaprl/support/tactics/dtactic.mli
+1 -1 metaprl/support/tactics/simp_typeinf.mli
+1 -1 metaprl/support/tactics/top_conversionals.ml
+1 -1 metaprl/support/tactics/top_conversionals.mli
+1 -1 metaprl/support/tactics/typeinf.mli
+1 -1 metaprl/support/tactics/var.mli
+23 -22 metaprl/tactics/proof/conversionals_boot.ml
+3 -6 metaprl/tactics/proof/conversionals_boot.mli
+0 -4 metaprl/tactics/proof/rewrite_boot.ml
+1 -7 metaprl/tactics/proof/rewrite_boot.mli
+2 -9 metaprl/tactics/proof/sequent_boot.ml
+1 -8 metaprl/tactics/proof/sequent_boot.mli
+2 -0 metaprl/tactics/proof/tactic_boot.mli
+34 -43 metaprl/tactics/proof/tactic_boot_sig.ml
+1 -1 metaprl/tactics/proof/tactic_type.ml
+12 -27 metaprl/tactics/proof/tactic_type.mli
+2 -7 metaprl/tactics/proof/tacticals_boot.ml
+1 -6 metaprl/tactics/proof/tacticals_boot.mli
+1 -1 metaprl/theories/base/base_rewrite.mli
+1 -12 metaprl/theories/cic/cic_ind_type.ml
+1 -1 metaprl/theories/czf/czf_itt_axioms.mli
+1 -1 metaprl/theories/czf/czf_itt_bool.mli
+1 -1 metaprl/theories/czf/czf_itt_cyclic_group.mli
+1 -2 metaprl/theories/czf/czf_itt_cyclic_subgroup.mli
+1 -9 metaprl/theories/czf/czf_itt_eq.ml
+1 -3 metaprl/theories/czf/czf_itt_eq.mli
+1 -10 metaprl/theories/czf/czf_itt_equiv.ml
+1 -3 metaprl/theories/czf/czf_itt_equiv.mli
+1 -1 metaprl/theories/czf/czf_itt_group.mli
+1 -1 metaprl/theories/czf/czf_itt_group_power.mli
+1 -2 metaprl/theories/czf/czf_itt_hom.mli
+1 -1 metaprl/theories/czf/czf_itt_inv_image.mli
+1 -2 metaprl/theories/czf/czf_itt_ker.mli
+1 -2 metaprl/theories/czf/czf_itt_member.mli
+1 -2 metaprl/theories/czf/czf_itt_nat.mli
+1 -2 metaprl/theories/czf/czf_itt_normal_subgroup.mli
+1 -1 metaprl/theories/czf/czf_itt_power.mli
+1 -1 metaprl/theories/czf/czf_itt_sall.mli
+1 -1 metaprl/theories/czf/czf_itt_sep.mli
+1 -9 metaprl/theories/czf/czf_itt_set.ml
+1 -3 metaprl/theories/czf/czf_itt_set.mli
+1 -6 metaprl/theories/czf/czf_itt_set_ind.ml
+1 -1 metaprl/theories/czf/czf_itt_setdiff.mli
+1 -1 metaprl/theories/czf/czf_itt_sexists.mli
+1 -2 metaprl/theories/czf/czf_itt_subgroup.mli
+1 -1 metaprl/theories/czf/czf_itt_union.mli
+1 -8 metaprl/theories/experimental/compile/m_closure.ml
+1 -2 metaprl/theories/experimental/compile/m_closure.mli
+1 -6 metaprl/theories/experimental/compile/m_cps.ml
+1 -1 metaprl/theories/experimental/compile/m_cps.mli
+1 -5 metaprl/theories/experimental/compile/m_dead.ml
+1 -1 metaprl/theories/experimental/compile/m_dead.mli
+1 -1 metaprl/theories/experimental/compile/m_inline.mli
+1 -6 metaprl/theories/experimental/compile/m_ir_ast.ml
+1 -2 metaprl/theories/experimental/compile/m_ir_ast.mli
+1 -4 metaprl/theories/experimental/compile/m_prog.ml
+1 -2 metaprl/theories/experimental/compile/m_prog.mli
+1 -1 metaprl/theories/experimental/compile/m_reserve.mli
+1 -1 metaprl/theories/experimental/compile/m_standardize.mli
+1 -1 metaprl/theories/experimental/compile/m_theory.mli
+1 -1 metaprl/theories/experimental/compile/m_util.mli
+1 -2 metaprl/theories/experimental/compile/m_x86_coalesce.mli
+1 -1 metaprl/theories/experimental/compile/m_x86_codegen.mli
+1 -5 metaprl/theories/experimental/compile/m_x86_opt.ml
+1 -2 metaprl/theories/experimental/compile/m_x86_opt.mli
+1 -1 metaprl/theories/experimental/compile/m_x86_regalloc.mli
+2 -8 metaprl/theories/experimental/compile/m_x86_spill.ml
+1 -3 metaprl/theories/experimental/compile/m_x86_spill.mli
+1 -1 metaprl/theories/fir/mfir_bool.mli
+1 -1 metaprl/theories/fir/mfir_int.mli
+1 -1 metaprl/theories/fir/mfir_int_set.mli
+1 -1 metaprl/theories/fir/mfir_list.mli
+1 -1 metaprl/theories/fir/mfir_record.mli
+1 -1 metaprl/theories/fir/mfir_token.mli
+1 -1 metaprl/theories/fir/mfir_tr_atom_base.mli
+1 -1 metaprl/theories/fir/mfir_util.mli
+1 -1 metaprl/theories/fol/cfol_itt_base.mli
+1 -1 metaprl/theories/fol/cfol_magic.mli
+1 -1 metaprl/theories/fol/fol_itt_and.mli
+1 -1 metaprl/theories/fol/fol_itt_implies.mli
+1 -1 metaprl/theories/fol/fol_itt_or.mli
+1 -1 metaprl/theories/fol/fol_itt_type.mli
+1 -1 metaprl/theories/fol/fol_prop.mli
+1 -2 metaprl/theories/fol/fol_struct.mli
+1 -2 metaprl/theories/itt/itt_atom.mli
+1 -1 metaprl/theories/itt/itt_atom_bool.mli
+1 -1 metaprl/theories/itt/itt_bintree.mli
+1 -2 metaprl/theories/itt/itt_bool.mli
+1 -1 metaprl/theories/itt/itt_bunion.mli
+1 -2 metaprl/theories/itt/itt_collection.mli
+1 -1 metaprl/theories/itt/itt_cyclic_group.mli
+1 -2 metaprl/theories/itt/itt_decidable.mli
+5 -6 metaprl/theories/itt/itt_derive.mli
+1 -2 metaprl/theories/itt/itt_dfun.mli
+1 -3 metaprl/theories/itt/itt_disect.mli
+4 -16 metaprl/theories/itt/itt_equal.ml
+1 -7 metaprl/theories/itt/itt_equal.mli
+1 -1 metaprl/theories/itt/itt_esquash.mli
+1 -1 metaprl/theories/itt/itt_eta.ml
+1 -2 metaprl/theories/itt/itt_eta.mli
+1 -1 metaprl/theories/itt/itt_example.mli
+2 -2 metaprl/theories/itt/itt_field2.mli
+1 -1 metaprl/theories/itt/itt_field_e.mli
+2 -8 metaprl/theories/itt/itt_fset.ml
+1 -2 metaprl/theories/itt/itt_fset.mli
+1 -7 metaprl/theories/itt/itt_fun.ml
+1 -2 metaprl/theories/itt/itt_fun.mli
+1 -1 metaprl/theories/itt/itt_group.mli
+1 -3 metaprl/theories/itt/itt_grouplikeobj.ml
+1 -1 metaprl/theories/itt/itt_grouplikeobj.mli
+2 -13 metaprl/theories/itt/itt_int_arith.ml
+1 -2 metaprl/theories/itt/itt_int_arith.mli
+2 -9 metaprl/theories/itt/itt_int_base.ml
+1 -3 metaprl/theories/itt/itt_int_base.mli
+1 -2 metaprl/theories/itt/itt_int_ext.mli
+2 -2 metaprl/theories/itt/itt_intdomain.mli
+1 -1 metaprl/theories/itt/itt_intdomain_e.mli
+1 -7 metaprl/theories/itt/itt_isect.ml
+1 -2 metaprl/theories/itt/itt_list2.mli
+4 -17 metaprl/theories/itt/itt_logic.ml
+1 -4 metaprl/theories/itt/itt_logic.mli
+1 -14 metaprl/theories/itt/itt_mpoly.ml
+2 -13 metaprl/theories/itt/itt_mpoly2.ml
+1 -2 metaprl/theories/itt/itt_mpoly2.mli
+1 -6 metaprl/theories/itt/itt_mpoly2_bench.ml
+2 -13 metaprl/theories/itt/itt_mpoly3.ml
+1 -2 metaprl/theories/itt/itt_mpoly3.mli
+1 -6 metaprl/theories/itt/itt_mpoly3_bench.ml
+1 -3 metaprl/theories/itt/itt_nat.mli
+1 -1 metaprl/theories/itt/itt_nequal.mli
+1 -1 metaprl/theories/itt/itt_order.mli
+1 -1 metaprl/theories/itt/itt_poly.mli
+1 -1 metaprl/theories/itt/itt_prop_decide.mli
+2 -8 metaprl/theories/itt/itt_quotient.ml
+1 -3 metaprl/theories/itt/itt_quotient.mli
+1 -1 metaprl/theories/itt/itt_quotient_group.mli
+1 -7 metaprl/theories/itt/itt_rat.ml
+1 -2 metaprl/theories/itt/itt_rat.mli
+1 -2 metaprl/theories/itt/itt_record.mli
+1 -1 metaprl/theories/itt/itt_record0.mli
+1 -1 metaprl/theories/itt/itt_record_exm.mli
+3 -12 metaprl/theories/itt/itt_record_label.ml
+1 -2 metaprl/theories/itt/itt_record_label.mli
+1 -2 metaprl/theories/itt/itt_record_label0.mli
+1 -2 metaprl/theories/itt/itt_record_renaming.mli
+1 -1 metaprl/theories/itt/itt_relation_str.mli
+1 -6 metaprl/theories/itt/itt_rfun.ml
+1 -3 metaprl/theories/itt/itt_rfun.mli
+1 -3 metaprl/theories/itt/itt_ring2.ml
+1 -1 metaprl/theories/itt/itt_ring2.mli
+1 -1 metaprl/theories/itt/itt_ring_e.mli
+1 -1 metaprl/theories/itt/itt_ring_uce.mli
+1 -1 metaprl/theories/itt/itt_sort.mli
+2 -14 metaprl/theories/itt/itt_squash.ml
+2 -5 metaprl/theories/itt/itt_squash.mli
+1 -8 metaprl/theories/itt/itt_squiggle.ml
+1 -2 metaprl/theories/itt/itt_squiggle.mli
+1 -7 metaprl/theories/itt/itt_struct.ml
+1 -2 metaprl/theories/itt/itt_struct.mli
+1 -9 metaprl/theories/itt/itt_struct2.ml
+1 -2 metaprl/theories/itt/itt_struct2.mli
+1 -2 metaprl/theories/itt/itt_struct3.mli
+1 -2 metaprl/theories/itt/itt_subset.mli
+1 -7 metaprl/theories/itt/itt_subtype.ml
+1 -2 metaprl/theories/itt/itt_subtype.mli
+2 -5 metaprl/theories/itt/itt_supinf.ml
+1 -1 metaprl/theories/itt/itt_supinf.mli
+1 -1 metaprl/theories/itt/itt_test.mli
+1 -5 metaprl/theories/itt/itt_union.ml
+2 -2 metaprl/theories/itt/itt_unitring.mli
+1 -10 metaprl/theories/mesa/ma_decidable__equality.ml
+1 -9 metaprl/theories/sil/sil_itt_sos.ml
+1 -2 metaprl/theories/sil/sil_itt_sos.mli
+1 -7 metaprl/theories/tptp/tptp.ml
+1 -3 metaprl/theories/tptp/tptp.mli
+1 -10 metaprl/theories/tptp/tptp_prove.ml
+5 -5 metaprl/theories/tptp/tptp_prove.mli