Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-02-14 22:59:08 -0800 (Tue, 14 Feb 2006)
Revision: 8705
Log message:

      - Filter_reflection: module names should not be capitalized.
      
      - OMakefile_theories: rules for generating .p4 and .p4i for the reflected
        theories (these are pretty-printed versions of the generated OCaml code;
        useful for debugging the filter).
      
      - OMakefile_theories: in rev 8704 I've ordered the new dependencies for the
        reflect_% files incorrectly (the theory .SUBDIRS did not have them in
        scope); fixed.
      
      - Filter_prog: generate the show_loading debugging call at the beginning and
        end of every theory.
      
      - A _huge_ number of theory files: removed the manual "show_loading" calls as
        they will now be automatically generated.
      

Changes  Path
+17 -12 metaprl/OMakefile_theories
+5 -2 metaprl/filter/filter/filter_prog.ml
+4 -4 metaprl/filter/filter/filter_reflect.ml
+0 -5 metaprl/support/display/base_dform.ml
+0 -2 metaprl/support/display/ocaml_base_df.ml
+0 -3 metaprl/support/display/ocaml_expr_df.ml
+0 -2 metaprl/support/display/ocaml_me_df.ml
+0 -2 metaprl/support/display/ocaml_mt_df.ml
+0 -3 metaprl/support/display/ocaml_patt_df.ml
+0 -3 metaprl/support/display/ocaml_sig_df.ml
+0 -3 metaprl/support/display/ocaml_str_df.ml
+0 -2 metaprl/support/display/ocaml_type_df.ml
+0 -5 metaprl/support/display/perv.ml
+0 -5 metaprl/support/display/summary.ml
+1 -1 metaprl/support/editor/nuprl_eval.ml
+0 -2 metaprl/support/editor/nuprl_run.ml
+0 -2 metaprl/support/editor/shell_mp.ml
+0 -5 metaprl/support/shell/package_info.ml
+0 -5 metaprl/support/shell/proof_edit.ml
+0 -2 metaprl/support/tactics/auto_tactic.ml
+0 -5 metaprl/support/tactics/dtactic.ml
+0 -5 metaprl/support/tactics/simp_typeinf.ml
+0 -5 metaprl/support/tactics/tactic_cache.ml
+1 -3 metaprl/support/tactics/top_conversionals.ml
+0 -5 metaprl/support/tactics/typeinf.ml
+0 -5 metaprl/support/tactics/var.ml
+0 -2 metaprl/theories/czf/czf_itt_abel_group.ml
+0 -2 metaprl/theories/czf/czf_itt_all.ml
+0 -2 metaprl/theories/czf/czf_itt_and.ml
+0 -2 metaprl/theories/czf/czf_itt_axioms.ml
+0 -2 metaprl/theories/czf/czf_itt_coset.ml
+0 -2 metaprl/theories/czf/czf_itt_cyclic_group.ml
+0 -2 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+0 -2 metaprl/theories/czf/czf_itt_dall.ml
+0 -2 metaprl/theories/czf/czf_itt_dexists.ml
+0 -2 metaprl/theories/czf/czf_itt_empty.ml
+0 -2 metaprl/theories/czf/czf_itt_equiv.ml
+0 -6 metaprl/theories/czf/czf_itt_exists.ml
+0 -2 metaprl/theories/czf/czf_itt_false.ml
+0 -2 metaprl/theories/czf/czf_itt_group.ml
+0 -2 metaprl/theories/czf/czf_itt_group_bvd.ml
+0 -2 metaprl/theories/czf/czf_itt_group_power.ml
+0 -2 metaprl/theories/czf/czf_itt_hom.ml
+0 -2 metaprl/theories/czf/czf_itt_implies.ml
+0 -2 metaprl/theories/czf/czf_itt_inv_image.ml
+0 -2 metaprl/theories/czf/czf_itt_isect.ml
+0 -2 metaprl/theories/czf/czf_itt_iso.ml
+0 -2 metaprl/theories/czf/czf_itt_ker.ml
+0 -2 metaprl/theories/czf/czf_itt_kleingroup.ml
+0 -2 metaprl/theories/czf/czf_itt_normal_subgroup.ml
+0 -2 metaprl/theories/czf/czf_itt_or.ml
+0 -2 metaprl/theories/czf/czf_itt_sall.ml
+0 -2 metaprl/theories/czf/czf_itt_sep.ml
+0 -2 metaprl/theories/czf/czf_itt_set.ml
+0 -2 metaprl/theories/czf/czf_itt_set_bvd.ml
+0 -2 metaprl/theories/czf/czf_itt_set_ind.ml
+0 -2 metaprl/theories/czf/czf_itt_setdiff.ml
+0 -2 metaprl/theories/czf/czf_itt_sexists.ml
+0 -2 metaprl/theories/czf/czf_itt_singleton.ml
+0 -2 metaprl/theories/czf/czf_itt_subgroup.ml
+0 -2 metaprl/theories/czf/czf_itt_true.ml
+0 -2 metaprl/theories/czf/czf_itt_union.ml
+0 -2 metaprl/theories/itt/applications/algebra/itt_field2.ml
+0 -2 metaprl/theories/itt/applications/algebra/itt_field_e.ml
+0 -2 metaprl/theories/itt/applications/algebra/itt_group.ml
+0 -2 metaprl/theories/itt/applications/algebra/itt_grouplikeobj.ml
+0 -2 metaprl/theories/itt/applications/algebra/itt_intdomain.ml
+0 -2 metaprl/theories/itt/applications/algebra/itt_intdomain_e.ml
+0 -2 metaprl/theories/itt/applications/algebra/itt_ring2.ml
+0 -2 metaprl/theories/itt/applications/algebra/itt_ring_e.ml
+0 -2 metaprl/theories/itt/applications/algebra/itt_ring_uce.ml
+0 -2 metaprl/theories/itt/applications/algebra/itt_unitring.ml
+0 -5 metaprl/theories/itt/applications/datatypes/itt_bintree.ml
+0 -6 metaprl/theories/itt/applications/datatypes/itt_datatree.ml
+0 -5 metaprl/theories/itt/applications/datatypes/itt_rbtree.ml
+0 -5 metaprl/theories/itt/applications/datatypes/itt_sortedtree.ml
+0 -2 metaprl/theories/itt/applications/supinf/itt_order.ml
+0 -1 metaprl/theories/itt/applications/supinf/itt_supinf.ml
+0 -6 metaprl/theories/itt/core/itt_atom.ml
+0 -2 metaprl/theories/itt/core/itt_decidable.ml
+0 -5 metaprl/theories/itt/core/itt_dfun.ml
+0 -6 metaprl/theories/itt/core/itt_dprod.ml
+0 -5 metaprl/theories/itt/core/itt_equal.ml
+2 -6 metaprl/theories/itt/core/itt_ext_equal.ml
+0 -1 metaprl/theories/itt/core/itt_int_base.ml
+0 -1 metaprl/theories/itt/core/itt_int_ext.ml
+0 -5 metaprl/theories/itt/core/itt_isect.ml
+0 -5 metaprl/theories/itt/core/itt_logic.ml
+0 -1 metaprl/theories/itt/core/itt_omega.ml
+0 -6 metaprl/theories/itt/core/itt_prec.ml
+0 -6 metaprl/theories/itt/core/itt_prod.ml
+0 -6 metaprl/theories/itt/core/itt_quotient.ml
+0 -5 metaprl/theories/itt/core/itt_record.ml
+0 -5 metaprl/theories/itt/core/itt_record0.ml
+0 -5 metaprl/theories/itt/core/itt_set.ml
+2 -6 metaprl/theories/itt/core/itt_singleton.ml
+0 -5 metaprl/theories/itt/core/itt_squash.ml
+0 -5 metaprl/theories/itt/core/itt_squiggle.ml
+0 -5 metaprl/theories/itt/core/itt_srec.ml
+0 -5 metaprl/theories/itt/core/itt_struct.ml
+0 -6 metaprl/theories/itt/core/itt_struct2.ml
+0 -5 metaprl/theories/itt/core/itt_subset.ml
+0 -5 metaprl/theories/itt/core/itt_subset2.ml
+0 -6 metaprl/theories/itt/core/itt_subtype.ml
+4 -8 metaprl/theories/itt/core/itt_union.ml
+0 -5 metaprl/theories/itt/core/itt_unit.ml
+0 -5 metaprl/theories/itt/core/itt_void.ml
+0 -5 metaprl/theories/itt/extensions/base/ctt_markov.ml
+0 -4 metaprl/theories/itt/extensions/pointwise/itt_pointwise.ml
+0 -6 metaprl/theories/itt/extensions/pointwise/itt_pointwise2.ml
+0 -6 metaprl/theories/itt/extensions/pointwise/itt_pointwise_struct3.ml
+0 -5 metaprl/theories/itt/extensions/rfun/itt_dfun_imp.ml
+0 -6 metaprl/theories/itt/extensions/rfun/itt_dprod_imp.ml
+0 -6 metaprl/theories/itt/extensions/rfun/itt_rfun.ml
+0 -2 metaprl/theories/ocaml_sos/ocaml_expr_sos.ml
+0 -2 metaprl/theories/ocaml_sos/ocaml_logic.ml
+0 -2 metaprl/theories/ocaml_sos/ocaml_me_sos.ml
+0 -2 metaprl/theories/ocaml_sos/ocaml_mt_sos.ml
+0 -2 metaprl/theories/ocaml_sos/ocaml_patt_sos.ml
+0 -2 metaprl/theories/ocaml_sos/ocaml_sig_sos.ml
+0 -2 metaprl/theories/ocaml_sos/ocaml_str_sos.ml
+0 -2 metaprl/theories/ocaml_sos/ocaml_type_sos.ml
+0 -5 metaprl/theories/s4lp/s4_logic.ml