Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-01 12:58:04 -0700 (Thu, 01 Sep 2005)
Revision: 7694
Log message:

      - Xin, we are no longer using "operator" = "bterm" approach (in fact, we are
      no longer using explicit bterms at all - bterms are just an external concent).
      
      - Added a configure test for htmldoc.
      

Changes  Path
+19 -11 metaprl/doc/OMakefile
+4 -10 metaprl/theories/itt/itt_hoas_operator.ml
+1 -1 metaprl/theories/itt/itt_reflection_new.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-01 13:09:46 -0700 (Thu, 01 Sep 2005)
Revision: 7695
Log message:

      More on concrete operators.
      

Changes  Path
+1 -3 metaprl/theories/base/base_operator.mli
+6 -10 metaprl/theories/itt/itt_hoas_operator.ml
+0 -2 metaprl/theories/itt/itt_hoas_operator.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-02 14:08:56 -0700 (Fri, 02 Sep 2005)
Revision: 7696
Log message:

      Revised the text on functors.
      

Changes  Path
Properties metaprl/theories/ocaml_doc/objects
Added metaprl/theories/ocaml_doc/objects/program1.ml
Properties metaprl/theories/ocaml_doc/objects/program1.ml
Added metaprl/theories/ocaml_doc/objects/program2.ml
Properties metaprl/theories/ocaml_doc/objects/program2.ml
+156 -184 metaprl/theories/ocaml_doc/ocaml_doc_mod3.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-09-02 14:09:36 -0700 (Fri, 02 Sep 2005)
Revision: 7697
Log message:

      Forgot these files.
      

Changes  Path
Added metaprl/theories/ocaml_doc/programs/setfunctor.ml
Properties metaprl/theories/ocaml_doc/programs/setfunctor.ml
Added metaprl/theories/ocaml_doc/programs/setfunctor2.ml
Properties metaprl/theories/ocaml_doc/programs/setfunctor2.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-02 17:30:03 -0700 (Fri, 02 Sep 2005)
Revision: 7698
Log message:

      *** WARNING: Breaks binary compatibility ***
      
      Implemented the "Operator" parameters that allow imbedding reflected
      "operators" into terms. This is similar to the recently introduces Shape
      parameters.
      

Changes  Path
+8 -7 metaprl/filter/base/filter_cache_fun.ml
+6 -4 metaprl/filter/base/filter_magic.ml
+7 -0 metaprl/filter/base/filter_summary.ml
+3 -0 metaprl/filter/filter/filter_parse.ml
+4 -0 metaprl/filter/filter/filter_patt.ml
+2 -0 metaprl/filter/filter/filter_prog.ml
+27 -6 metaprl/filter/filter/term_grammar.ml
+2 -2 metaprl/library/mbterm.ml
+41 -13 metaprl/refiner/refiner/refiner_debug.ml
+17 -11 metaprl/refiner/reflib/ascii_io.ml
+4 -1 metaprl/refiner/reflib/ascii_io_sig.ml
+7 -1 metaprl/refiner/reflib/dform.ml
+20 -13 metaprl/refiner/reflib/simple_print.ml
+2 -0 metaprl/refiner/reflib/term_hash_code.ml
+17 -0 metaprl/refiner/reflib/term_order.ml
+4 -0 metaprl/refiner/reflib/term_ty_infer.ml
+1 -0 metaprl/refiner/refsig/refiner_sig.ml
+4 -2 metaprl/refiner/refsig/rewrite_sig.ml
+4 -0 metaprl/refiner/refsig/term_shape_sig.ml
+11 -2 metaprl/refiner/refsig/term_sig.ml
+2 -0 metaprl/refiner/refsig/term_subst_minimal_sig.ml
+5 -3 metaprl/refiner/refsig/term_subst_sig.ml
+1 -0 metaprl/refiner/refsig/term_ty_sig.ml
+4 -0 metaprl/refiner/refsig/termmod_sig.ml
+10 -2 metaprl/refiner/rewrite/rewrite.ml
+2 -1 metaprl/refiner/rewrite/rewrite.mli
+15 -2 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+1 -1 metaprl/refiner/rewrite/rewrite_build_contractum.mli
+10 -0 metaprl/refiner/rewrite/rewrite_compile_contractum.ml
+2 -0 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+11 -3 metaprl/refiner/rewrite/rewrite_debug.ml
+1 -1 metaprl/refiner/rewrite/rewrite_debug.mli
+20 -1 metaprl/refiner/rewrite/rewrite_match_redex.ml
+1 -1 metaprl/refiner/rewrite/rewrite_match_redex.mli
+4 -0 metaprl/refiner/rewrite/rewrite_types.ml
+1 -1 metaprl/refiner/term_ds/term_ds.ml
+1 -1 metaprl/refiner/term_ds/term_ds_sig.ml
+5 -0 metaprl/refiner/term_ds/term_man_ds.ml
+17 -2 metaprl/refiner/term_ds/term_subst_ds.ml
+2 -1 metaprl/refiner/term_gen/term_header_constr.ml
+5 -0 metaprl/refiner/term_gen/term_man_gen.ml
+47 -36 metaprl/refiner/term_gen/term_shape_gen.ml
+3 -1 metaprl/refiner/term_gen/term_ty_gen.ml
+1 -1 metaprl/refiner/term_std/term_std.ml
+1 -1 metaprl/refiner/term_std/term_std_sig.ml
+17 -2 metaprl/refiner/term_std/term_subst_std.ml
+1 -0 metaprl/support/display/perv.mli
+14 -7 metaprl/theories/base/base_meta.ml
+5 -0 metaprl/theories/base/base_meta.mli
+13 -68 metaprl/theories/base/base_operator.ml
+1 -3 metaprl/theories/base/base_operator.mli
+6 -6 metaprl/theories/itt/itt_hoas_operator.ml
+2 -0 metaprl/util/gen_refiner_debug.pl

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-03 16:34:04 -0700 (Sat, 03 Sep 2005)
Revision: 7699
Log message:

      RefineError -> RefineForceError.
      

Changes  Path
+1 -1 metaprl/theories/itt/itt_logic.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-09-03 16:40:57 -0700 (Sat, 03 Sep 2005)
Revision: 7700
Log message:

      Use LexStringSet instead of StringSet in UI.
      

Changes  Path
+6 -6 metaprl/support/shell/package_info.ml

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-09-04 20:57:18 -0700 (Sun, 04 Sep 2005)
Revision: 7701
Log message:

      One unification rule that was introduced for multi-modal case
      was applied too generously - similar result could be obtained
      by more than one sequence of rules. Hence we were wasting some time
      in unification. This commit limits that rule application to
      only one case where it really needed.
      

Changes  Path
+1 -1 metaprl/refiner/reflib/jtunify.ml

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-09-05 10:20:34 -0700 (Mon, 05 Sep 2005)
Revision: 7702
Log message:

      Made multimodal-specific rule more narrow
      

Changes  Path
+1 -1 metaprl/refiner/reflib/jtunify.ml

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-09-05 10:42:30 -0700 (Mon, 05 Sep 2005)
Revision: 7703
Log message:

      Removed one more redundant application of the multi-modal rule.
      

Changes  Path
+1 -1 metaprl/refiner/reflib/jtunify.ml

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-09-05 12:59:41 -0700 (Mon, 05 Sep 2005)
Revision: 7704
Log message:

      More tests
      

Changes  Path
+6 -0 metaprl/theories/s4lp/s4_tests.ml
+934 -849 metaprl/theories/s4lp/s4_tests.prla

Changes by: Limin Jia (ljia at CS.Princeton.EDU)
Date: 2005-09-06 07:05:35 -0700 (Tue, 06 Sep 2005)
Revision: 7705
Log message:

      Add examples
      

Changes  Path
+7 -0 metaprl/theories/ilc/OMakefile
+14 -4 metaprl/theories/ilc/ilc_core.ml
+2 -0 metaprl/theories/ilc/ilc_core.mli
Added metaprl/theories/ilc/ilc_extend.ml
Properties metaprl/theories/ilc/ilc_extend.ml
Added metaprl/theories/ilc/ilc_extend.mli
Properties metaprl/theories/ilc/ilc_extend.mli
Added metaprl/theories/ilc/ilc_listtest.ml
Properties metaprl/theories/ilc/ilc_listtest.ml
Added metaprl/theories/ilc/ilc_listtest.mli
Properties metaprl/theories/ilc/ilc_listtest.mli
Added metaprl/theories/ilc/ilc_listtest1.ml
Properties metaprl/theories/ilc/ilc_listtest1.ml
Added metaprl/theories/ilc/ilc_listtest1.mli
Properties metaprl/theories/ilc/ilc_listtest1.mli
Added metaprl/theories/ilc/ilc_longmergesort.ml
Properties metaprl/theories/ilc/ilc_longmergesort.ml
Added metaprl/theories/ilc/ilc_longmergesort.mli
Properties metaprl/theories/ilc/ilc_longmergesort.mli
Added metaprl/theories/ilc/ilc_mergesort.ml
Properties metaprl/theories/ilc/ilc_mergesort.ml
Added metaprl/theories/ilc/ilc_mergesort.mli
Properties metaprl/theories/ilc/ilc_mergesort.mli
Added metaprl/theories/ilc/ilc_term.ml
Properties metaprl/theories/ilc/ilc_term.ml
Added metaprl/theories/ilc/ilc_term.mli
Properties metaprl/theories/ilc/ilc_term.mli
Added metaprl/theories/ilc/ilc_test.ml
Properties metaprl/theories/ilc/ilc_test.ml
Added metaprl/theories/ilc/ilc_test.mli
Properties metaprl/theories/ilc/ilc_test.mli

Changes by: ( at unknown.email)
Date: 2005-09-06 07:05:35 -0700 (Tue, 06 Sep 2005)
Revision: 7706
Log message:

      This commit was manufactured by cvs2svn to create branch
      'omake_0_9_7_pre6'.

Changes  Path
Copied metaprl-branches/omake_0_9_7_pre6
Deleted metaprl-branches/omake_0_9_7_pre6/BUGS
Deleted metaprl-branches/omake_0_9_7_pre6/Makefile
Deleted metaprl-branches/omake_0_9_7_pre6/README
Deleted metaprl-branches/omake_0_9_7_pre6/README.MACOSX
Deleted metaprl-branches/omake_0_9_7_pre6/README.WIN32
Deleted metaprl-branches/omake_0_9_7_pre6/clib/c_time.c
Deleted metaprl-branches/omake_0_9_7_pre6/clib/debug.c
Deleted metaprl-branches/omake_0_9_7_pre6/clib/debug.h
Deleted metaprl-branches/omake_0_9_7_pre6/clib/execvp.c
Deleted metaprl-branches/omake_0_9_7_pre6/clib/exit.c
Deleted metaprl-branches/omake_0_9_7_pre6/clib/inextern.h
Deleted metaprl-branches/omake_0_9_7_pre6/clib/locale.c
Deleted metaprl-branches/omake_0_9_7_pre6/clib/ml_debug.c
Deleted metaprl-branches/omake_0_9_7_pre6/clib/ml_debug.h
Deleted metaprl-branches/omake_0_9_7_pre6/clib/print_symbols.c
Deleted metaprl-branches/omake_0_9_7_pre6/clib/print_symbols.h
Deleted metaprl-branches/omake_0_9_7_pre6/clib/profile.c
Deleted metaprl-branches/omake_0_9_7_pre6/clib/putenv.c
Deleted metaprl-branches/omake_0_9_7_pre6/clib/termsize.c
Deleted metaprl-branches/omake_0_9_7_pre6/clib/truncate.c
Deleted metaprl-branches/omake_0_9_7_pre6/debug/debug.ml
Deleted metaprl-branches/omake_0_9_7_pre6/debug/debug.mli
Deleted metaprl-branches/omake_0_9_7_pre6/debug/debug_symbols.ml
Deleted metaprl-branches/omake_0_9_7_pre6/debug/debug_symbols.mli
Deleted metaprl-branches/omake_0_9_7_pre6/doc/itt_quickref.txt
Deleted metaprl-branches/omake_0_9_7_pre6/doc/latex/theories/README
Deleted metaprl-branches/omake_0_9_7_pre6/doc/latex/theories/all-theories.tex
Deleted metaprl-branches/omake_0_9_7_pre6/doc/parser.txt
Deleted metaprl-branches/omake_0_9_7_pre6/doc/resources_spec.txt
Deleted metaprl-branches/omake_0_9_7_pre6/doc/status.tex
Deleted metaprl-branches/omake_0_9_7_pre6/doc/weblintrc
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/.gdbinit
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/BOO008-3.p
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/GEN.p
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/QUICKSTART
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/make_mp_version.ml
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mp
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mp.ml
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mp.mli
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mp_top.ml
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mp_top.mli
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mp_version.mli
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mpconfig
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mpdebug
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mpdebug-top
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mpgossip
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mpkonsole
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mpkonsole-large
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mpopt
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mpopt.bat
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mpserver
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mpshell
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mptop
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mptop.bat
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mpxterm
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/mpxterm-large
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/nuprl_eval.ml
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/nuprl_eval.mli
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/nuprl_jprover.ml
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/nuprl_jprover.mli
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/nuprl_run.ml
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/nuprl_run.mli
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/nuprl_sig.mlz
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/shell_mp.ml
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/shell_mp.mli
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/shell_p4.ml
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/shell_p4.mli
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/tutorial.ml
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/tutorial_itt.ml
Deleted metaprl-branches/omake_0_9_7_pre6/editor/ml/x.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_buffer.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_buffer.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_cache.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_cache.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_cache_fun.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_cache_fun.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_exn.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_exn.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_grammar.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_grammar.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_hash.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_hash.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_magic.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_magic.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_ocaml.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_ocaml.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_spell.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_spell.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_summary.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_summary.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_summary_io.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_summary_io.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_summary_param.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_summary_type.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_summary_util.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_summary_util.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_type.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_util.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/filter_util.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/free_vars.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/free_vars.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/infix.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/base/infix.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/filter_bin.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/filter_bin.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/filter_convert.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/filter_convert.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/filter_main.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/filter_main.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/filter_parse.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/filter_parse.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/filter_patt.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/filter_patt.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/filter_prog.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/filter_prog.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/prlcomp.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/prlcomp.mli
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/term_grammar.ml
Deleted metaprl-branches/omake_0_9_7_pre6/filter/filter/term_grammar.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/ascii_scan.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/ascii_scan.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/basic.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/basic.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/bigInt.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/bigInt.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/db.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/db.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/definition.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/definition.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/library.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/library.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/library_type_base.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/library_type_base.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/link.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/link.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/lint32.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/lint32.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/mathBus.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/mathBus.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/mbs-mpl.txt
Deleted metaprl-branches/omake_0_9_7_pre6/library/mbterm.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/mbterm.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/nuprl5.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/nuprl5.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/object_id.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/object_id.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/oidtable.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/oidtable.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/orb.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/orb.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/registry.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/registry.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/registry.txt
Deleted metaprl-branches/omake_0_9_7_pre6/library/socketIo.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/socketIo.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/tentfunctor.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/tentfunctor.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/test.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/test.mli
Deleted metaprl-branches/omake_0_9_7_pre6/library/utils.ml
Deleted metaprl-branches/omake_0_9_7_pre6/library/utils.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mk/config.local.empty
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/array_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/bitset.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/bitset.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/comment_parse.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/comment_parse.mll
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/ctime.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/ctime.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/debug_string_sets.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/debug_string_sets.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/debug_tables.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/debug_tables.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/env_arg.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/env_arg.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/file_base.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/file_base.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/file_base_type.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/file_type_base.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/file_type_base.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/flist.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/flist.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/hash_with_gc.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/hash_with_gc.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/hash_with_gc_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/http_server.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/http_server.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/http_server_type.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/http_simple.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/http_simple.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/index.html
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/line_buffer.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/line_buffer.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/list_neq_append.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/list_neq_append.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/memo.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/memo.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/memo_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/mp_term.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/mp_term.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/permutations.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/permutations.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/precedence.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/precedence.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/punix.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/punix.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/remote_lazy_queue.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/remote_lazy_queue.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/remote_lazy_queue_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/remote_queue_null.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/remote_queue_null.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/remote_queue_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/setup.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/setup.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/simplehash_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/simplehashtbl.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/simplehashtbl.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/weak_memo.ml
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/weak_memo.mli
Deleted metaprl-branches/omake_0_9_7_pre6/mllib/weak_memo_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/proxyedit/proxyedit_lex.mli
Deleted metaprl-branches/omake_0_9_7_pre6/proxyedit/proxyedit_lex.mll
Deleted metaprl-branches/omake_0_9_7_pre6/proxyedit/proxyedit_main.ml
Deleted metaprl-branches/omake_0_9_7_pre6/proxyedit/proxyedit_main.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refbase/OMakefile
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refbase/opname.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refbase/opname.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refbase/seq_set.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refbase/seq_set.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/OMakefile
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/refine.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/refine.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/refine_error.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/refine_error.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/refiner.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/refiner.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/refiner_debug.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/refiner_debug.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/refiner_ds.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/refiner_ds.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/refiner_io.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/refiner_io.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/refiner_std.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refiner/refiner_std.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/OMakefile
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/arith.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/arith.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/ascii_io.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/ascii_io.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/ascii_io_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/dform.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/dform.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/jall.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/jall.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/jlogic_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/jordering.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/jtunify.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/jtunify.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/jtypes.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/lib_term.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/lib_term.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/match_seq.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/match_seq.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/ml_term.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/ml_term.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/mp_resource.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/mp_resource.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/refine_exn.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/refine_exn.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/simple_print.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/simple_print.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/simple_print_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/supinf.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/supinf.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_compare.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_compare.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_compare_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_copy2_weak.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_copy2_weak.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_copy_weak.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_copy_weak.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_dtable.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_dtable.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_eq_table.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_eq_table.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_hash_code.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_hash_code.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_io.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_io.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_match_table.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_match_table.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_order.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_order.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_stable.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_stable.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_ty_infer.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/term_ty_infer.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/theory.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/theory.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/unify_mm.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/reflib/unify_mm.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/OMakefile
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/refine_error.mlh
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/refine_error_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/refine_minimal_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/refine_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/refiner_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/rewrite_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/term_addr_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/term_base_minimal_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/term_base_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/term_hash_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/term_man_minimal_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/term_man_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/term_meta_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/term_norm_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/term_op_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/term_shape_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/term_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/term_subst_minimal_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/term_subst_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/term_ty_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/termmod_hash_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/termmod_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/refsig/thread_refiner_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_build_contractum.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_build_contractum.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_compile_contractum.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_compile_contractum.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_compile_redex.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_compile_redex.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_debug.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_debug.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_debug_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_match_redex.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_match_redex.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_types.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_util.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_util.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/rewrite/rewrite_util_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/rob_ds.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/rob_ds.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/term_addr_ds.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/term_addr_ds.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/term_base_ds.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/term_base_ds.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/term_ds.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/term_ds.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/term_ds_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/term_man_ds.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/term_man_ds.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/term_op_ds.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/term_op_ds.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/term_subst_ds.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_ds/term_subst_ds.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_addr_gen.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_addr_gen.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_hash.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_hash.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_header_constr.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_header_constr.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_man_gen.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_man_gen.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_man_gen_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_meta_gen.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_meta_gen.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_norm.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_norm.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_shape_gen.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_shape_gen.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_ty_gen.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_gen/term_ty_gen.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_std/term_base_std.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_std/term_base_std.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_std/term_op_std.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_std/term_op_std.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_std/term_std.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_std/term_std.mli
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_std/term_std_sig.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_std/term_subst_std.ml
Deleted metaprl-branches/omake_0_9_7_pre6/refiner/term_std/term_subst_std.mli
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/base_dform.ml
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/base_dform.mli
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/comment.ml
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/comment.mli
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/mpfont.ml
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/mpfont.mli
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/mpsymbols.ml
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/mpsymbols.mli
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/ocaml.mlz
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/ocaml_base_df.ml
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/ocaml_base_df.mli
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/ocaml_df.mlz
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/ocaml_expr_df.ml
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/ocaml_expr_df.mli
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/ocaml_me_df.ml
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/ocaml_me_df.mli
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/ocaml_mt_df.ml
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/ocaml_mt_df.mli
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/ocaml_patt_df.ml
Deleted metaprl-branches/omake_0_9_7_pre6/support/display/ocaml_patt_df.mli
Deleted