Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-08-27 12:38:57 -0700 (Wed, 27 Aug 2003)
Revision: 4883
Log message:

      - Removed (using the util/clean-opens script) approx. 2400 unneeded "open"
       statements. This will hopefully reduce the dependency tree size, reduce
      the dependency analysis time during compilation and possibly speed up
      some partial compilations.
      
      - Removed a number of blank lines (MetaPRL policy is to try not to have more
      than one blank line in a row)
      
      - A few minor changes to better disambiguate cases where two modules declare
      a type with the same name and both modules are opened.
      

Changes  Path
+0 -2 metaprl/editor/ml/nuprl_eval.ml
+0 -7 metaprl/editor/ml/nuprl_run.ml
+0 -1 metaprl/editor/ml/nuprl_sig.mlz
+0 -9 metaprl/editor/ml/shell_mp.ml
+1 -3 metaprl/filter/base/filter_ast.ml
+0 -2 metaprl/filter/base/filter_ast.mli
+0 -1 metaprl/filter/base/filter_buffer.ml
+0 -2 metaprl/filter/base/filter_cache.ml
+0 -1 metaprl/filter/base/filter_cache.mli
+0 -4 metaprl/filter/base/filter_cache_fun.ml
+0 -1 metaprl/filter/base/filter_cache_fun.mli
+0 -2 metaprl/filter/base/filter_comment.ml
+0 -3 metaprl/filter/base/filter_exn.ml
+0 -2 metaprl/filter/base/filter_exn.mli
+0 -2 metaprl/filter/base/filter_grammar.ml
+0 -1 metaprl/filter/base/filter_hash.ml
+0 -1 metaprl/filter/base/filter_magic.ml
+0 -1 metaprl/filter/base/filter_ocaml.mli
+0 -2 metaprl/filter/base/filter_summary.ml
+0 -1 metaprl/filter/base/filter_summary.mli
+0 -1 metaprl/filter/base/filter_summary_io.ml
+0 -2 metaprl/filter/base/filter_summary_io.mli
+0 -1 metaprl/filter/base/filter_summary_type.ml
+0 -3 metaprl/filter/base/filter_summary_util.ml
+0 -1 metaprl/filter/base/filter_summary_util.mli
+0 -4 metaprl/filter/base/filter_util.ml
+0 -1 metaprl/filter/base/filter_util.mli
+0 -1 metaprl/filter/base/infix.mli
+0 -1 metaprl/filter/base/mLast_util.ml
+0 -5 metaprl/filter/boot/conversionals_boot.ml
+0 -8 metaprl/filter/boot/proof_boot.ml
+0 -1 metaprl/filter/boot/proof_boot.mli
+0 -4 metaprl/filter/boot/proof_convert.ml
+0 -1 metaprl/filter/boot/proof_term_boot.ml
+0 -1 metaprl/filter/boot/proof_term_boot.mli
+0 -4 metaprl/filter/boot/rewrite_boot.ml
+0 -1 metaprl/filter/boot/sequent_boot.ml
+0 -5 metaprl/filter/boot/tactic_boot.ml
+0 -7 metaprl/filter/boot/tactic_boot_sig.mlz
+0 -1 metaprl/filter/boot/tactic_type.mli
+0 -3 metaprl/filter/boot/tacticals_boot.ml
+0 -1 metaprl/filter/boot/tacticals_boot.mli
+0 -2 metaprl/filter/filter/filter_bin.ml
+0 -6 metaprl/filter/filter/filter_convert.ml
+0 -5 metaprl/filter/filter/filter_parse.ml
+0 -1 metaprl/filter/filter/filter_parse.mli
+0 -7 metaprl/filter/filter/filter_patt.ml
+0 -1 metaprl/filter/filter/filter_patt.mli
+0 -5 metaprl/filter/filter/filter_prog.ml
+0 -1 metaprl/filter/filter/filter_prog.mli
+0 -6 metaprl/filter/filter/term_grammar.ml
+0 -3 metaprl/filter/filter/term_grammar.mli
+0 -1 metaprl/filter/phobos/filter_phobos.ml
+0 -2 metaprl/filter/phobos/phobos_compile.ml
+0 -2 metaprl/filter/phobos/phobos_exn.ml
+0 -2 metaprl/filter/phobos/phobos_exn.mli
+0 -2 metaprl/filter/phobos/phobos_grammar.ml
+0 -1 metaprl/filter/phobos/phobos_lexer.mll
+0 -5 metaprl/filter/phobos/phobos_main.ml
+0 -1 metaprl/filter/phobos/phobos_parse_state.ml
+0 -1 metaprl/filter/phobos/phobos_report.mli
+0 -3 metaprl/filter/phobos/phobos_rewrite.ml
+0 -4 metaprl/filter/phobos/phobos_rewrite.mli
+0 -4 metaprl/filter/phobos/phobos_token_inheritance.ml
+0 -6 metaprl/filter/phobos/phobos_token_inheritance.mli
+0 -2 metaprl/filter/phobos/phobos_tokenizer.ml
+0 -0 metaprl/filter/phobos/phobos_util.ml
+0 -1 metaprl/library/ascii_scan.ml
+0 -4 metaprl/library/basic.ml
+0 -1 metaprl/library/basic.mli
+225 -228 metaprl/library/db.ml
+0 -1 metaprl/library/definition.ml
+0 -2 metaprl/library/library.ml
+0 -1 metaprl/library/library_type_base.ml
+0 -1 metaprl/library/link.ml
+22 -23 metaprl/library/lint32.ml
+22 -22 metaprl/library/lint32.mli
+16 -17 metaprl/library/mathBus.ml
+23 -24 metaprl/library/mathBus.mli
+1 -3 metaprl/library/mbterm.ml
+0 -1 metaprl/library/mbterm.mli
+0 -3 metaprl/library/nuprl5.ml
+4 -5 metaprl/library/oidtable.ml
+0 -3 metaprl/library/orb.ml
+1 -2 metaprl/library/orb.mli
+5 -7 metaprl/library/registry.ml
+4 -4 metaprl/library/registry.mli
+0 -1 metaprl/library/socketIo.ml
+0 -1 metaprl/library/tentfunctor.ml
+0 -2 metaprl/library/utils.ml
+0 -1 metaprl/library/utils.mli
+0 -1 metaprl/mllib/bitset.ml
+0 -1 metaprl/mllib/file_type_base.ml
+0 -1 metaprl/mllib/precedence.ml
+0 -1 metaprl/mllib/weak_memo.ml
+0 -2 metaprl/refiner/refbase/opname.ml
+0 -1 metaprl/refiner/refiner/refine.ml
+0 -1 metaprl/refiner/refiner/refiner_ds.ml
+0 -2 metaprl/refiner/refiner/refiner_ds.mli
+0 -1 metaprl/refiner/refiner/refiner_std.ml
+0 -2 metaprl/refiner/refiner/refiner_std.mli
+0 -1 metaprl/refiner/reflib/arith.ml
+0 -1 metaprl/refiner/reflib/dform.ml
+0 -1 metaprl/refiner/reflib/dform.mli
+0 -1 metaprl/refiner/reflib/dform_print.ml
+0 -3 metaprl/refiner/reflib/dform_print.mli
+0 -1 metaprl/refiner/reflib/jall.ml
+0 -3 metaprl/refiner/reflib/jall.mli
+0 -4 metaprl/refiner/reflib/jlogic_sig.ml
+0 -6 metaprl/refiner/reflib/ml_file.ml
+0 -2 metaprl/refiner/reflib/ml_format.ml
+0 -1 metaprl/refiner/reflib/ml_format_sig.mlz
+0 -3 metaprl/refiner/reflib/ml_print.ml
+0 -1 metaprl/refiner/reflib/ml_print_sig.mlz
+0 -2 metaprl/refiner/reflib/ml_string.ml
+0 -3 metaprl/refiner/reflib/ml_term.ml
+0 -1 metaprl/refiner/reflib/ml_term.mli
+0 -1 metaprl/refiner/reflib/mp_resource.ml
+0 -1 metaprl/refiner/reflib/mp_resource.mli
+0 -4 metaprl/refiner/reflib/refine_exn.ml
+0 -1 metaprl/refiner/reflib/refine_exn.mli
+0 -1 metaprl/refiner/reflib/simple_print.ml
+0 -1 metaprl/refiner/reflib/simple_print_sig.ml
+0 -2 metaprl/refiner/reflib/term_compare.ml
+0 -1 metaprl/refiner/reflib/term_compare.mli
+0 -1 metaprl/refiner/reflib/term_copy2_weak.ml
+0 -1 metaprl/refiner/reflib/term_copy_weak.ml
+0 -4 metaprl/refiner/reflib/term_dtable.ml
+0 -1 metaprl/refiner/reflib/term_eq_table.ml
+0 -1 metaprl/refiner/reflib/term_io.ml
+0 -2 metaprl/refiner/reflib/term_match_table.ml
+0 -1 metaprl/refiner/reflib/term_match_table.mli
+0 -3 metaprl/refiner/reflib/term_stable.ml
+0 -2 metaprl/refiner/reflib/theory.ml
+0 -4 metaprl/refiner/reflib/unify_mm.ml
+0 -3 metaprl/refiner/reflib/unify_mm.mli
+0 -3 metaprl/refiner/refsig/refiner_sig.ml
+0 -1 metaprl/refiner/refsig/term_base_minimal_sig.ml
+0 -1 metaprl/refiner/refsig/term_hash_sig.ml
+0 -1 metaprl/refiner/refsig/term_sig.ml
+0 -1 metaprl/refiner/refsig/termmod_hash_sig.ml
+0 -1 metaprl/refiner/refsig/termmod_sig.ml
+0 -4 metaprl/refiner/rewrite/rewrite.ml
+0 -1 metaprl/refiner/rewrite/rewrite.mli
+0 -4 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+0 -1 metaprl/refiner/rewrite/rewrite_build_contractum.mli
+0 -4 metaprl/refiner/rewrite/rewrite_compile_contractum.ml
+0 -1 metaprl/refiner/rewrite/rewrite_compile_contractum.mli
+0 -5 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+0 -1 metaprl/refiner/rewrite/rewrite_compile_redex.mli
+0 -1 metaprl/refiner/rewrite/rewrite_debug.ml
+0 -1 metaprl/refiner/rewrite/rewrite_debug.mli
+0 -1 metaprl/refiner/rewrite/rewrite_debug_sig.ml
+0 -1 metaprl/refiner/rewrite/rewrite_match_redex.mli
+0 -3 metaprl/refiner/rewrite/rewrite_meta.ml
+0 -2 metaprl/refiner/rewrite/rewrite_meta.mli
+0 -1 metaprl/refiner/rewrite/rewrite_types.mli
+0 -3 metaprl/refiner/rewrite/rewrite_util.ml
+0 -1 metaprl/refiner/rewrite/rewrite_util.mli
+0 -3 metaprl/refiner/term_ds/term_addr_ds.ml
+0 -2 metaprl/refiner/term_ds/term_base_ds.mli
+0 -1 metaprl/refiner/term_ds/term_ds.ml
+0 -2 metaprl/refiner/term_ds/term_ds_sig.ml
+0 -1 metaprl/refiner/term_ds/term_man_ds.ml
+0 -3 metaprl/refiner/term_gen/term_addr_gen.ml
+0 -3 metaprl/refiner/term_gen/term_hash.ml
+0 -1 metaprl/refiner/term_gen/term_hash.mli
+0 -8 metaprl/refiner/term_gen/term_header_constr.ml
+0 -1 metaprl/refiner/term_gen/term_header_constr.mli
+0 -1 metaprl/refiner/term_gen/term_man_gen.ml
+0 -1 metaprl/refiner/term_gen/term_man_gen.mli
+0 -1 metaprl/refiner/term_gen/term_meta_gen.ml
+0 -2 metaprl/refiner/term_gen/term_norm.ml
+0 -1 metaprl/refiner/term_gen/term_norm.mli
+0 -1 metaprl/refiner/term_std/term_base_std.ml
+0 -2 metaprl/refiner/term_std/term_base_std.mli
+0 -1 metaprl/refiner/term_std/term_eval_std.ml
+0 -1 metaprl/refiner/term_std/term_op_std.ml
+0 -2 metaprl/refiner/term_std/term_std.ml
+0 -2 metaprl/refiner/term_std/term_std_sig.ml
+0 -2 metaprl/support/display/base_dform.ml
+0 -2 metaprl/support/display/nuprl_font.ml
+0 -2 metaprl/support/display/ocaml_base_df.ml
+0 -1 metaprl/support/display/ocaml_expr_df.ml
+0 -1 metaprl/support/display/ocaml_me_df.ml
+0 -1 metaprl/support/display/ocaml_mt_df.ml
+0 -1 metaprl/support/display/ocaml_patt_df.ml
+0 -1 metaprl/support/display/ocaml_sig_df.ml
+0 -1 metaprl/support/display/ocaml_str_df.ml
+0 -1 metaprl/support/display/ocaml_type_df.ml
+0 -3 metaprl/support/display/perv.ml
+0 -3 metaprl/support/display/summary.ml
+0 -4 metaprl/support/shell/display_term.ml
+0 -4 metaprl/support/shell/mptop.ml
+0 -2 metaprl/support/shell/mptop.mli
+0 -6 metaprl/support/shell/package_info.ml
+3 -6 metaprl/support/shell/package_sig.mlz
+0 -5 metaprl/support/shell/proof_edit.ml
+0 -1 metaprl/support/shell/proof_edit.mli
+0 -2 metaprl/support/shell/shell.ml
+0 -5 metaprl/support/shell/shell_p4_sig.mlz
+0 -4 metaprl/support/shell/shell_package.ml
+0 -7 metaprl/support/shell/shell_rewrite.ml
+0 -2 metaprl/support/shell/shell_root.ml
+0 -8 metaprl/support/shell/shell_rule.ml
+0 -3 metaprl/support/shell/shell_sig.mlz
+0 -2 metaprl/support/shell/shell_state.ml
+0 -3 metaprl/support/shell/shell_state.mli
+0 -7 metaprl/support/tactics/auto_tactic.ml
+0 -4 metaprl/support/tactics/auto_tactic.mli
+0 -1 metaprl/support/tactics/base_cache.ml
+0 -1 metaprl/support/tactics/base_cache.mli
+0 -1 metaprl/support/tactics/dtactic.ml
+0 -1 metaprl/support/tactics/dtactic.mli
+0 -10 metaprl/support/tactics/simp_typeinf.ml
+0 -2 metaprl/support/tactics/simp_typeinf.mli
+0 -2 metaprl/support/tactics/tactic_cache.ml
+0 -1 metaprl/support/tactics/tactic_cache.mli
+0 -4 metaprl/support/tactics/top_conversionals.ml
+0 -2 metaprl/support/tactics/top_conversionals.mli
+0 -1 metaprl/support/tactics/top_tacticals.ml
+2 -6 metaprl/support/tactics/top_tacticals.mli
+0 -4 metaprl/support/tactics/typeinf.ml
+0 -2 metaprl/support/tactics/typeinf.mli
+0 -2 metaprl/support/tactics/var.ml
+0 -9 metaprl/theories/base/base_rewrite.ml
+0 -1 metaprl/theories/base/base_rewrite.mli
+0 -17 metaprl/theories/czf/czf_itt_abel_group.ml
+0 -19 metaprl/theories/czf/czf_itt_abel_group.mli
+0 -16 metaprl/theories/czf/czf_itt_all.ml
+0 -8 metaprl/theories/czf/czf_itt_and.ml
+0 -3 metaprl/theories/czf/czf_itt_axioms.ml
+0 -19 metaprl/theories/czf/czf_itt_bool.ml
+0 -2 metaprl/theories/czf/czf_itt_bool.mli
+0 -14 metaprl/theories/czf/czf_itt_coset.ml
+0 -16 metaprl/theories/czf/czf_itt_coset.mli
+0 -17 metaprl/theories/czf/czf_itt_cyclic_group.ml
+0 -19 metaprl/theories/czf/czf_itt_cyclic_group.mli
+0 -17 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+0 -18 metaprl/theories/czf/czf_itt_cyclic_subgroup.mli
+0 -6 metaprl/theories/czf/czf_itt_dall.ml
+0 -1 metaprl/theories/czf/czf_itt_dall.mli
+0 -6 metaprl/theories/czf/czf_itt_dexists.ml
+0 -1 metaprl/theories/czf/czf_itt_dexists.mli
+0 -4 metaprl/theories/czf/czf_itt_empty.ml
+0 -5 metaprl/theories/czf/czf_itt_eq.ml
+0 -8 metaprl/theories/czf/czf_itt_equiv.ml
+0 -23 metaprl/theories/czf/czf_itt_equiv.mli
+0 -16 metaprl/theories/czf/czf_itt_exists.ml
+0 -4 metaprl/theories/czf/czf_itt_false.ml
+0 -18 metaprl/theories/czf/czf_itt_group.ml
+0 -18 metaprl/theories/czf/czf_itt_group.mli
+0 -18 metaprl/theories/czf/czf_itt_group_bvd.ml
+0 -20 metaprl/theories/czf/czf_itt_group_bvd.mli
+0 -17 metaprl/theories/czf/czf_itt_group_power.ml
+0 -19 metaprl/theories/czf/czf_itt_group_power.mli
+0 -18 metaprl/theories/czf/czf_itt_hom.ml
+0 -17 metaprl/theories/czf/czf_itt_hom.mli
+0 -8 metaprl/theories/czf/czf_itt_implies.ml
+0 -16 metaprl/theories/czf/czf_itt_inv_image.ml
+0 -18 metaprl/theories/czf/czf_itt_inv_image.mli
+0 -7 metaprl/theories/czf/czf_itt_isect.ml
+0 -18 metaprl/theories/czf/czf_itt_iso.ml
+0 -20 metaprl/theories/czf/czf_itt_iso.mli
+0 -18 metaprl/theories/czf/czf_itt_ker.ml
+0 -17 metaprl/theories/czf/czf_itt_ker.mli
+0 -18 metaprl/theories/czf/czf_itt_kleingroup.ml
+0 -20 metaprl/theories/czf/czf_itt_kleingroup.mli
+0 -7 metaprl/theories/czf/czf_itt_member.ml
+0 -1 metaprl/theories/czf/czf_itt_member.mli
+0 -4 metaprl/theories/czf/czf_itt_nat.ml
+0 -1 metaprl/theories/czf/czf_itt_nat.mli
+0 -14 metaprl/theories/czf/czf_itt_normal_subgroup.ml
+0 -14 metaprl/theories/czf/czf_itt_normal_subgroup.mli
+0 -8 metaprl/theories/czf/czf_itt_or.ml
+0 -1 metaprl/theories/czf/czf_itt_power.ml
+0 -1 metaprl/theories/czf/czf_itt_power.mli
+0 -2 metaprl/theories/czf/czf_itt_rel.ml
+0 -6 metaprl/theories/czf/czf_itt_sall.ml
+0 -1 metaprl/theories/czf/czf_itt_sall.mli
+0 -6 metaprl/theories/czf/czf_itt_sep.ml
+0 -1 metaprl/theories/czf/czf_itt_sep.mli
+0 -14 metaprl/theories/czf/czf_itt_set.ml
+0 -2 metaprl/theories/czf/czf_itt_set.mli
+0 -16 metaprl/theories/czf/czf_itt_set_bvd.ml
+0 -19 metaprl/theories/czf/czf_itt_set_bvd.mli
+0 -5 metaprl/theories/czf/czf_itt_set_ind.ml
+0 -18 metaprl/theories/czf/czf_itt_setdiff.ml
+0 -9 metaprl/theories/czf/czf_itt_setdiff.mli
+0 -6 metaprl/theories/czf/czf_itt_sexists.ml
+0 -4 metaprl/theories/czf/czf_itt_singleton.ml
+0 -14 metaprl/theories/czf/czf_itt_subgroup.ml
+0 -11 metaprl/theories/czf/czf_itt_subgroup.mli
+0 -4 metaprl/theories/czf/czf_itt_true.ml
+0 -6 metaprl/theories/czf/czf_itt_union.ml
+0 -2 metaprl/theories/experimental/compile/m_ast.ml
+0 -2 metaprl/theories/experimental/compile/m_ast.mli
+0 -6 metaprl/theories/experimental/compile/m_closure.ml
+0 -1 metaprl/theories/experimental/compile/m_closure.mli
+0 -8 metaprl/theories/experimental/compile/m_cps.ml
+0 -3 metaprl/theories/experimental/compile/m_cps.mli
+0 -2 metaprl/theories/experimental/compile/m_dead.ml
+0 -1 metaprl/theories/experimental/compile/m_dead.mli
+0 -1 metaprl/theories/experimental/compile/m_ir_ast.ml
+0 -3 metaprl/theories/experimental/compile/m_ir_ast.mli
+0 -11 metaprl/theories/experimental/compile/m_prog.ml
+0 -2 metaprl/theories/experimental/compile/m_prog.mli
+0 -3 metaprl/theories/experimental/compile/m_ra_main.ml
+0 -1 metaprl/theories/experimental/compile/m_standardize.ml
+0 -0 metaprl/theories/experimental/compile/m_test.ml
+0 -2 metaprl/theories/experimental/compile/m_theory.ml
+0 -2 metaprl/theories/experimental/compile/m_util.ml
+0 -5 metaprl/theories/experimental/compile/m_x86_codegen.ml
+0 -2 metaprl/theories/experimental/compile/m_x86_codegen.mli
+0 -1 metaprl/theories/experimental/compile/m_x86_frame.ml
+0 -1 metaprl/theories/experimental/compile/m_x86_opt.ml
+0 -1 metaprl/theories/experimental/compile/m_x86_opt.mli
+0 -3 metaprl/theories/experimental/compile/m_x86_regalloc.ml
+0 -7 metaprl/theories/experimental/compile/m_x86_spill.ml
+0 -3 metaprl/theories/experimental/compile/m_x86_spill.mli
+0 -2 metaprl/theories/experimental/compile/m_x86_term.ml
+0 -1 metaprl/theories/fir/mfir_termOp_base.ml
+0 -1 metaprl/theories/fir/mfir_token.ml
+0 -1 metaprl/theories/fir/mfir_ty.ml
+0 -1 metaprl/theories/fir/mfir_ty.mli
+0 -2 metaprl/theories/fol/cfol_itt_base.ml
+0 -1 metaprl/theories/fol/cfol_itt_base.mli
+0 -1 metaprl/theories/fol/cfol_magic.ml
+0 -1 metaprl/theories/fol/fol_false.ml
+0 -1 metaprl/theories/fol/fol_pred.ml
+0 -1 metaprl/theories/fol/fol_prop.ml
+0 -16 metaprl/theories/itt/ctt_markov.ml
+0 -15 metaprl/theories/itt/itt_algebra_df.ml
+0 -7 metaprl/theories/itt/itt_atom.ml
+0 -5 metaprl/theories/itt/itt_atom_bool.ml
+0 -15 metaprl/theories/itt/itt_bintree.ml
+0 -20 metaprl/theories/itt/itt_bintree.mli
+0 -8 metaprl/theories/itt/itt_bisect.ml
+0 -7 metaprl/theories/itt/itt_bool.ml
+0 -1 metaprl/theories/itt/itt_bool.mli
+0 -10 metaprl/theories/itt/itt_bunion.ml
+0 -10 metaprl/theories/itt/itt_collection.ml
+0 -6 metaprl/theories/itt/itt_collection.mli
+0 -18 metaprl/theories/itt/itt_cyclic_group.ml
+0 -19 metaprl/theories/itt/itt_cyclic_group.mli
+0 -15 metaprl/theories/itt/itt_datatree.ml
+0 -4 metaprl/theories/itt/itt_datatree.mli
+0 -8 metaprl/theories/itt/itt_decidable.ml
+0 -2 metaprl/theories/itt/itt_decidable.mli
+0 -4 metaprl/theories/itt/itt_derive.ml
+0 -12 metaprl/theories/itt/itt_dfun.ml
+0 -1 metaprl/theories/itt/itt_dfun.mli
+0 -7 metaprl/theories/itt/itt_disect.ml
+0 -11 metaprl/theories/itt/itt_dprod.ml
+0 -1 metaprl/theories/itt/itt_dprod.mli
+0 -6 metaprl/theories/itt/itt_equal.ml
+0 -3 metaprl/theories/itt/itt_equal.mli
+0 -1 metaprl/theories/itt/itt_esquash.mli
+0 -1 metaprl/theories/itt/itt_eta.mli
+0 -3 metaprl/theories/itt/itt_ext_equal.ml
+0 -1 metaprl/theories/itt/itt_ext_equal.mli
+0 -7 metaprl/theories/itt/itt_fset.ml
+0 -1 metaprl/theories/itt/itt_fset.mli
+0 -5 metaprl/theories/itt/itt_fun.ml
+0 -1 metaprl/theories/itt/itt_fun.mli
+0 -20 metaprl/theories/itt/itt_group.ml
+0 -19 metaprl/theories/itt/itt_group.mli
+0 -20 metaprl/theories/itt/itt_grouplikeobj.ml
+0 -19 metaprl/theories/itt/itt_grouplikeobj.mli
+0 -5 metaprl/theories/itt/itt_int_arith.ml
+0 -4 metaprl/theories/itt/itt_int_arith.mli
+0 -7 metaprl/theories/itt/itt_int_base.ml
+0 -2 metaprl/theories/itt/itt_int_base.mli
+0 -13 metaprl/theories/itt/itt_int_ext.ml
+0 -1 metaprl/theories/itt/itt_int_ext.mli
+0 -13 metaprl/theories/itt/itt_inv_typing.ml
+0 -15 metaprl/theories/itt/itt_inv_typing.mli
+0 -4 metaprl/theories/itt/itt_isect.ml
+0 -1 metaprl/theories/itt/itt_isect.mli
+0 -11 metaprl/theories/itt/itt_list.ml
+0 -1 metaprl/theories/itt/itt_list.mli
+0 -11 metaprl/theories/itt/itt_list2.ml
+0 -1 metaprl/theories/itt/itt_list2.mli
+0 -4 metaprl/theories/itt/itt_logic.ml
+0 -1 metaprl/theories/itt/itt_logic.mli
+0 -16 metaprl/theories/itt/itt_nat.ml
+0 -15 metaprl/theories/itt/itt_pointwise.ml
+0 -16 metaprl/theories/itt/itt_pointwise2.ml
+0 -5 metaprl/theories/itt/itt_prec.ml
+0 -9 metaprl/theories/itt/itt_prod.ml
+0 -1 metaprl/theories/itt/itt_prod.mli
+0 -3 metaprl/theories/itt/itt_prop_decide.ml
+0 -4 metaprl/theories/itt/itt_quotient.ml
+0 -13 metaprl/theories/itt/itt_rbtree.ml
+0 -4 metaprl/theories/itt/itt_rbtree.mli
+0 -11 metaprl/theories/itt/itt_record.ml
+0 -2 metaprl/theories/itt/itt_record.mli
+0 -15 metaprl/theories/itt/itt_record0.ml
+0 -4 metaprl/theories/itt/itt_record0.mli
+0 -16 metaprl/theories/itt/itt_record_exm.ml
+0 -4 metaprl/theories/itt/itt_record_exm.mli
+0 -13 metaprl/theories/itt/itt_record_label.ml
+0 -2 metaprl/theories/itt/itt_record_label.mli
+0 -8 metaprl/theories/itt/itt_record_label0.ml
+0 -4 metaprl/theories/itt/itt_record_label0.mli
+0 -15 metaprl/theories/itt/itt_relation_str.ml
+0 -2 metaprl/theories/itt/itt_relation_str.mli
+0 -11 metaprl/theories/itt/itt_rfun.ml
+0 -11 metaprl/theories/itt/itt_set.ml
+0 -1 metaprl/theories/itt/itt_set.mli
+0 -17 metaprl/theories/itt/itt_set_str.ml
+0 -4 metaprl/theories/itt/itt_set_str.mli
+0 -21 metaprl/theories/itt/itt_singleton.ml
+0 -5 metaprl/theories/itt/itt_sort.ml
+0 -1 metaprl/theories/itt/itt_sort.mli
+0 -12 metaprl/theories/itt/itt_sortedtree.ml
+0 -4 metaprl/theories/itt/itt_sortedtree.mli
+0 -3 metaprl/theories/itt/itt_squash.ml
+0 -1 metaprl/theories/itt/itt_squash.mli
+0 -9 metaprl/theories/itt/itt_squiggle.ml
+0 -3 metaprl/theories/itt/itt_squiggle.mli
+1 -9 metaprl/theories/itt/itt_srec.ml
+0 -8 metaprl/theories/itt/itt_struct.ml
+0 -1 metaprl/theories/itt/itt_struct.mli
+0 -8 metaprl/theories/itt/itt_struct2.ml
+0 -1 metaprl/theories/itt/itt_struct2.mli
+0 -14 metaprl/theories/itt/itt_struct3.ml
+0 -15 metaprl/theories/itt/itt_struct3.mli
+0 -17 metaprl/theories/itt/itt_subset.ml
+0 -1 metaprl/theories/itt/itt_subset.mli
+0 -23 metaprl/theories/itt/itt_subset2.ml
+0 -4 metaprl/theories/itt/itt_subset2.mli
+0 -5 metaprl/theories/itt/itt_subtype.ml
+0 -1 metaprl/theories/itt/itt_subtype.mli
+0 -2 metaprl/theories/itt/itt_theory.ml
+0 -12 metaprl/theories/itt/itt_tsquash.ml
+0 -4 metaprl/theories/itt/itt_tunion.ml
+0 -9 metaprl/theories/itt/itt_union.ml
+0 -1 metaprl/theories/itt/itt_union.mli
+0 -1 metaprl/theories/itt/itt_union2.ml
+0 -8 metaprl/theories/itt/itt_unit.ml
+0 -1 metaprl/theories/itt/itt_unit.mli
+0 -6 metaprl/theories/itt/itt_void.ml
+0 -1 metaprl/theories/itt/itt_void.mli
+0 -10 metaprl/theories/itt/itt_w.ml
+0 -2 metaprl/theories/ocaml_doc/ocaml_doc_mod1.ml
+0 -2 metaprl/theories/phobos/phobos_base.ml
+0 -5 metaprl/theories/phobos/phobos_base.mli
+0 -2 metaprl/theories/sil/sil_itt_sos.ml
+0 -1 metaprl/theories/sil/sil_itt_sos.mli
+0 -4 metaprl/theories/tptp/tptp.ml
+0 -1 metaprl/theories/tptp/tptp.mli
+0 -2 metaprl/theories/tptp/tptp_cache.ml
+0 -2 metaprl/theories/tptp/tptp_load.ml
+0 -1 metaprl/theories/tptp/tptp_parse.mly
+0 -5 metaprl/theories/tptp/tptp_prove.ml
+0 -2 metaprl/theories/tptp/tptp_prove.mli
Added metaprl/util/clean-opens
Properties metaprl/util/clean-opens
+0 -1 metaprl/util/ocamldep.mll
+0 -4 mpcompiler/mmc/core/core_sequent.ml
+0 -2 mpcompiler/mmc/core/core_sequent.mli
+0 -10 mpcompiler/mmc/core/core_tuple.ml
+0 -3 mpcompiler/mmc/core/mmc_core_closure.ml
+0 -1 mpcompiler/mmc/core/mmc_core_cps.mli
+0 -1 mpcompiler/mmc/core/mmc_core_name.ml
+0 -2 mpcompiler/mmc/core/mmc_core_name.mli
+0 -6 mpcompiler/mmc/core/mmc_core_type_check.ml
+0 -2 mpcompiler/mmc/core/mmc_core_type_erase.ml
+0 -2 mpcompiler/mmc/core/mmc_core_type_erase.mli
+0 -6 mpcompiler/mmc/core/mmc_core_type_infer.ml
+0 -3 mpcompiler/mmc/core/mmc_core_type_infer.mli
+0 -2 mpcompiler/mmc/core/mmc_core_type_util.ml
+0 -1 mpcompiler/mmc/core/mmc_core_type_util.mli
+0 -2 mpcompiler/mmc/core/mmc_core_util.ml
+0 -17 mpcompiler/mmc/extensions/ext_arithmetic.ml
+0 -22 mpcompiler/mmc/extensions/ext_arithmetic_integer.ml
+0 -17 mpcompiler/mmc/extensions/ext_array.ml
+0 -3 mpcompiler/mmc/extensions/ext_integer.ml