Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-16 15:50:32 -0700 (Wed, 16 Jul 2008)
Revision: 13137
Log message:

      Fix all the theory files.

Changes  Path(relative to metaprl-branches/ocaml-3.10.0)
+3 -0 filter/base/filter_exn.ml
+1 -1 filter/filter/filter_bin.ml
+6 -7 filter/filter/term_grammar.ml
+5 -1 mk/vars
+52 -52 theories/cic/cic_ind_elim.ml
+39 -39 theories/cic/cic_ind_elim.mli
+153 -153 theories/cic/cic_ind_elim_dep.ml
+59 -59 theories/cic/cic_ind_elim_dep.mli
+5 -5 theories/cic/cic_ind_type.ml
+4 -4 theories/cic/cic_ind_type.mli
+2 -2 theories/czf/czf_itt_coset.ml
+2 -2 theories/czf/czf_itt_group_bvd.ml
+1 -1 theories/czf/czf_itt_group_bvd.mli
+1 -1 theories/czf/czf_itt_hom.ml
+2 -2 theories/czf/czf_itt_subgroup.ml
+1 -1 theories/czf/czf_itt_subgroup.mli
+5 -5 theories/czf/czf_itt_subset.ml
+2 -2 theories/czf/czf_itt_subset.mli
+1 -1 theories/experimental/compile/m_arith.ml
+1 -1 theories/experimental/compile/m_closure.ml
+1 -1 theories/experimental/compile/m_dead.ml
+1 -1 theories/experimental/compile/m_prog.ml
+2 -2 theories/experimental/compile/m_x86_opt.ml
+1 -1 theories/experimental/compile/m_x86_spill.ml
+5 -5 theories/fir/mfir_int_set.ml
+1 -1 theories/itt/applications/algebra/itt_field2.ml
+1 -1 theories/itt/applications/algebra/itt_field_e.ml
+8 -8 theories/itt/applications/algebra/itt_group.ml
+5 -5 theories/itt/applications/algebra/itt_grouplikeobj.ml
+1 -1 theories/itt/applications/algebra/itt_intdomain.ml
+1 -1 theories/itt/applications/algebra/itt_intdomain_e.ml
+2 -2 theories/itt/applications/algebra/itt_ring2.ml
+1 -1 theories/itt/applications/algebra/itt_ring_e.ml
+1 -1 theories/itt/applications/algebra/itt_ring_uce.ml
+1 -1 theories/itt/applications/datatypes/itt_bintree.ml
+8 -8 theories/itt/applications/datatypes/itt_rbtree.ml
+8 -8 theories/itt/applications/datatypes/itt_set_str.ml
+4 -4 theories/itt/applications/datatypes/itt_sort.ml
+2 -2 theories/itt/applications/datatypes/itt_sortedtree.ml
+1 -1 theories/itt/applications/function_spaces/itt_closure.ml
+1 -1 theories/itt/applications/function_spaces/itt_functions.ml
+3 -3 theories/itt/extensions/base/itt_antiquotient.ml
+8 -8 theories/itt/extensions/rfun/itt_dfun_imp.ml
+7 -7 theories/itt/extensions/rfun/itt_dfun_imp.mli
+3 -3 theories/itt/extensions/rfun/itt_dprod_imp.ml
+4 -4 theories/itt/extensions/rfun/itt_rfun.ml
+1 -1 theories/itt/extensions/vector/itt_vec_bind.ml
+9 -9 theories/itt/extensions/vector/itt_vec_list1.ml
+1 -1 theories/itt/extensions/vector/itt_vec_sequent_term.ml
+1 -1 theories/itt/reflection/core/itt_hoas_vbind.ml
+1 -1 theories/itt/reflection/experimental/itt_hoas_bterm.ml
+2 -2 theories/itt/reflection/experimental/itt_hoas_bterm_wf.ml
+3 -3 theories/itt/reflection/experimental/itt_hoas_lof.ml
+3 -3 theories/itt/reflection/experimental/itt_hoas_normalize.ml
+3 -3 theories/itt/reflection/experimental/itt_hoas_sequent.ml
+2 -2 theories/itt/reflection/experimental/itt_hoas_sequent_normalize.ml
+6 -6 theories/itt/reflection/experimental/itt_hoas_sequent_term.ml
+9 -9 theories/itt/reflection/experimental/itt_hoas_sequent_term_wf.ml
+4 -3 theories/itt/reflection/experimental/itt_hoas_util.ml
+4 -3 theories/meta/extensions/meta_dtactic.ml
+2 -2 theories/meta/extensions/meta_implies.ml
+2 -2 theories/tptp/tptp_load.ml
+1 -1 theories/tptp/tptp_prove.ml