Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-03-30 13:52:05 -0800 (Thu, 30 Mar 2006)
Revision: 8972
Log message:

      Use options instead of exceptions in get_with_arg/get_with_args/get_univ_arg
      (as we are catching these exceptions right away almost everywhere).
      

Changes  Path
+29 -5 metaprl/support/tactics/dtactic.ml
+4 -0 metaprl/support/tactics/dtactic.mli
+4 -2 metaprl/support/tactics/forward.ml
+3 -3 metaprl/support/tactics/simp_typeinf.ml
+8 -10 metaprl/support/tactics/typeinf.ml
+6 -13 metaprl/support/tactics/var.ml
+2 -1 metaprl/tactics/proof/sequent_boot.ml
+3 -7 metaprl/tactics/proof/tactic_boot.ml
+9 -9 metaprl/tactics/proof/tactic_boot_sig.ml
+3 -5 metaprl/tactics/proof/tacticals_boot.ml
+16 -30 metaprl/theories/czf/czf_itt_equiv.ml
+8 -18 metaprl/theories/itt/applications/datatypes/itt_collection.ml
+21 -15 metaprl/theories/itt/applications/datatypes/itt_fset.ml
+10 -13 metaprl/theories/itt/applications/datatypes/itt_sort.ml
+12 -11 metaprl/theories/itt/core/itt_bisect.ml
+6 -3 metaprl/theories/itt/core/itt_bool.ml
+7 -10 metaprl/theories/itt/core/itt_dfun.ml
+7 -7 metaprl/theories/itt/core/itt_disect.ml
+8 -13 metaprl/theories/itt/core/itt_isect.ml
+4 -2 metaprl/theories/itt/core/itt_list2.ml
+3 -3 metaprl/theories/itt/core/itt_logic.ml
+3 -2 metaprl/theories/itt/core/itt_struct.ml
+5 -5 metaprl/theories/itt/core/itt_struct2.ml
+39 -5 metaprl/theories/itt/core/itt_struct3.ml
+5 -7 metaprl/theories/itt/core/itt_subtype.ml
+40 -10 metaprl/theories/itt/extensions/pointwise/itt_pointwise_struct3.ml
+11 -12 metaprl/theories/itt/extensions/rfun/itt_dfun_imp.ml
+3 -5 metaprl/theories/itt/reflection/experimental/itt_hoas_bterm_wf.ml
+5 -4 metaprl/theories/meta/extensions/meta_context_ind1.ml
+8 -4 metaprl/theories/meta/extensions/meta_dtactic.ml
+3 -3 metaprl/theories/tptp/tptp_derive.ml