Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-17 13:39:18 -0800 (Tue, 17 Jan 2006)
Revision: 8494
Log message:

      Changes to options:
      
         - Options are now based on opnames, so that we don't get
           accidental collisions between unrelated theories.
      
         - The tactic_arg options are OptionAllow and OptionExclude.
           So
      
              # Allow rules labeled with the given opname
              withAllowOptionT : term -> tactic -> tactic
      
              # Exclude rules labeled with the given opname
              withExcludeOptionT : term -> tactic -> tactic
      
           To make this work, we need to extend option annotations
           for rules.  Not done yet.
      
         - The Top_options.select resource can be used to specify
           default options for a theory.
      
           [Ping Aleksey]  I get confused by Mp_resource.  Currently,
           theory-local resources are pruned during close_theory.
           I don't know if this works.
      

Changes  Path
+1 -0 metaprl/refiner/reflib/dform.ml
+93 -54 metaprl/refiner/reflib/mp_resource.ml
+8 -6 metaprl/refiner/reflib/mp_resource.mli
+8 -6 metaprl/refiner/reflib/term_match_table.ml
+4 -3 metaprl/refiner/reflib/term_stable.ml
+8 -6 metaprl/support/shell/browser_resource.ml
+4 -3 metaprl/support/shell/mptop.ml
+1 -0 metaprl/support/tactics/OMakefile
+3 -1 metaprl/support/tactics/auto_tactic.ml
+4 -3 metaprl/support/tactics/base_cache.ml
+1 -0 metaprl/support/tactics/basic_tactics.ml
+31 -32 metaprl/support/tactics/dtactic.ml
+12 -6 metaprl/support/tactics/dtactic.mli
+16 -14 metaprl/support/tactics/top_conversionals.ml
+4 -3 metaprl/support/tactics/top_conversionals.mli
Added metaprl/support/tactics/top_options.ml
Properties metaprl/support/tactics/top_options.ml
Added metaprl/support/tactics/top_options.mli
Properties metaprl/support/tactics/top_options.mli
+2 -7 metaprl/support/tactics/top_tacticals.ml
+0 -5 metaprl/support/tactics/top_tacticals.mli
+2 -0 metaprl/tactics/proof/sequent_boot.ml
+51 -6 metaprl/tactics/proof/tactic_boot.ml
+18 -6 metaprl/tactics/proof/tactic_boot_sig.ml
+4 -8 metaprl/tactics/proof/tacticals_boot.ml
+1 -1 metaprl/theories/itt/applications/algebra/itt_field2.ml
+1 -1 metaprl/theories/itt/applications/algebra/itt_field_e.ml
+5 -5 metaprl/theories/itt/applications/algebra/itt_group.ml
+5 -5 metaprl/theories/itt/applications/algebra/itt_grouplikeobj.ml
+1 -1 metaprl/theories/itt/applications/algebra/itt_intdomain.ml
+1 -1 metaprl/theories/itt/applications/algebra/itt_intdomain_e.ml
+2 -2 metaprl/theories/itt/applications/algebra/itt_ring2.ml
+1 -1 metaprl/theories/itt/applications/algebra/itt_ring_e.ml
+1 -1 metaprl/theories/itt/applications/algebra/itt_ring_uce.ml
+1 -1 metaprl/theories/itt/applications/datatypes/itt_bintree.ml
+2 -2 metaprl/theories/itt/applications/datatypes/itt_relation_str.ml
+2 -2 metaprl/theories/itt/applications/datatypes/itt_sortedtree.ml
+1 -1 metaprl/theories/itt/applications/function_spaces/itt_closure.ml
+1 -1 metaprl/theories/itt/applications/objects/itt_union_of.ml
+12 -12 metaprl/theories/itt/applications/supinf/itt_order.ml
+1 -1 metaprl/theories/itt/core/itt_atom_bool.ml
+2 -2 metaprl/theories/itt/core/itt_bisect.ml
+2 -2 metaprl/theories/itt/core/itt_dfun.ml
+2 -2 metaprl/theories/itt/core/itt_disect.ml
+2 -2 metaprl/theories/itt/core/itt_esquash.ml
+1 -1 metaprl/theories/itt/core/itt_ext_equal.ml
+10 -10 metaprl/theories/itt/core/itt_int_ext.ml
+1 -1 metaprl/theories/itt/core/itt_isect.ml
+1 -6 metaprl/theories/itt/core/itt_logic.ml
+2 -2 metaprl/theories/itt/core/itt_omega.ml
+2 -2 metaprl/theories/itt/core/itt_quotient.ml
+5 -5 metaprl/theories/itt/core/itt_record.ml
+2 -2 metaprl/theories/itt/core/itt_record_exm.ml
+2 -2 metaprl/theories/itt/core/itt_record_label.ml
+1 -0 metaprl/theories/itt/core/itt_sqsimple.ml
+1 -1 metaprl/theories/itt/core/itt_squash.ml
+3 -2 metaprl/theories/itt/core/itt_subtype.ml
+1 -1 metaprl/theories/itt/extensions/rfun/itt_dfun_imp.ml
+2 -1 metaprl/theories/itt/reflection/experimental/itt_hoas_relax1.ml
+6 -6 metaprl/theories/itt/reflection/experimental/itt_hoas_util.ml
+1 -0 metaprl/theories/meta/base/base_theory.mlz
+21 -33 metaprl/theories/meta/extensions/meta_dtactic.ml
+7 -5 metaprl/theories/meta/extensions/meta_dtactic.mli
+1 -1 metaprl/theories/meta/extensions/meta_implies.ml