Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-03 16:18:38 -0700 (Thu, 03 Jul 2003)
Revision: 4693
Log message:

      Added some example code for how we want new term
      constructors and destructors in core_type_infer.ml.
      This code doesn't compile, but it demonstrates the
      concept.
      

Changes  Path
+1 -1 metaprl/editor/ml/mpconfig
+3 -3 metaprl/support/tactics/simp_typeinf.ml
+1 -1 mpcompiler/mmc/core/mmc_core_ast.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-03 16:19:36 -0700 (Thu, 03 Jul 2003)
Revision: 4694
Log message:

      Forgot to add the file.
      

Changes  Path
Added mpcompiler/mmc/core/mmc_core_type_infer.ml
Properties mpcompiler/mmc/core/mmc_core_type_infer.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-03 20:56:03 -0700 (Thu, 03 Jul 2003)
Revision: 4697
Log message:

      Beginning the slow process of migrating MetaPRL toward libmojave.
      

Changes  Path
+1 -1 metaprl/Makefile
+8 -3 metaprl/OMakefile
+9 -15 metaprl/editor/ml/OMakefile
+4 -0 metaprl/mk/make_config.sh
+1 -1 mpcompiler/mmc/core/mmc_core_type_infer.ml

Changes by: ( at unknown.email)
Date: 2003-07-04 13:52:30 -0700 (Fri, 04 Jul 2003)
Revision: 4700
Log message:

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

Changes  Path
Copied metaprl-branches/abstract_vars
Copied mpcompiler-branches/abstract_vars
Copied texinputs-branches/abstract_vars
Deleted texinputs-branches/abstract_vars/1cm.sty
Deleted texinputs-branches/abstract_vars/1cml.sty
Deleted texinputs-branches/abstract_vars/Makefile
Deleted texinputs-branches/abstract_vars/Makefile-common
Deleted texinputs-branches/abstract_vars/PPR-macros.tex
Deleted texinputs-branches/abstract_vars/PPRmyppr.sty
Deleted texinputs-branches/abstract_vars/bcp.bib
Deleted texinputs-branches/abstract_vars/citlogo.eps
Deleted texinputs-branches/abstract_vars/citlogo2.eps
Deleted texinputs-branches/abstract_vars/config.ppr
Deleted texinputs-branches/abstract_vars/cornell-logo.eps
Deleted texinputs-branches/abstract_vars/dag50.eps
Deleted texinputs-branches/abstract_vars/der.tex
Deleted texinputs-branches/abstract_vars/gate.eps
Deleted texinputs-branches/abstract_vars/gate.pdf
Deleted texinputs-branches/abstract_vars/include.tex
Deleted texinputs-branches/abstract_vars/llncs.cls
Deleted texinputs-branches/abstract_vars/omscmsy.fd
Deleted texinputs-branches/abstract_vars/ot1cmr.fd
Deleted texinputs-branches/abstract_vars/ot1cmss.fd
Deleted texinputs-branches/abstract_vars/ot1lcmss.fd
Deleted texinputs-branches/abstract_vars/ot1lcmtt.fd
Deleted texinputs-branches/abstract_vars/pprpdf
Deleted texinputs-branches/abstract_vars/proof.sty
Deleted texinputs-branches/abstract_vars/slides-nogin.cls
Deleted texinputs-branches/abstract_vars/splncs.bst
Deleted texinputs-branches/abstract_vars/umsa.fd
Deleted texinputs-branches/abstract_vars/umsb.fd

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-06 16:41:01 -0700 (Sun, 06 Jul 2003)
Revision: 4704
Log message:

      I decided to finish the port to abstract vars anyway.
      
      This versdion compiles with omake.  Will fix make next.
      

Changes  Path
+27 -55 metaprl-branches/abstract_vars/editor/ml/nuprl_eval.ml
+5 -4 metaprl-branches/abstract_vars/filter/base/filter_summary.ml
+4 -3 metaprl-branches/abstract_vars/refiner/reflib/mp_resource.ml
+2 -1 metaprl-branches/abstract_vars/refiner/reflib/mp_resource.mli
+8 -6 metaprl-branches/abstract_vars/support/display/base_dform.ml
+6 -6 metaprl-branches/abstract_vars/support/shell/shell_package.ml
+1 -1 metaprl-branches/abstract_vars/support/shell/shell_rewrite.ml
+13 -68 metaprl-branches/abstract_vars/support/tactics/top_tacticals.ml
+2 -1 metaprl-branches/abstract_vars/theories/base/base_meta.ml
+5 -4 metaprl-branches/abstract_vars/theories/czf/czf_itt_eq.mli
+5 -4 metaprl-branches/abstract_vars/theories/czf/czf_itt_equiv.mli
+2 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_rel.mli
+3 -2 metaprl-branches/abstract_vars/theories/czf/czf_itt_set.mli
+1 -0 metaprl-branches/abstract_vars/theories/itt/itt_derive.ml
+3 -2 metaprl-branches/abstract_vars/theories/itt/itt_disect.mli
+16 -46 metaprl-branches/abstract_vars/theories/itt/itt_dprod.ml
+5 -4 metaprl-branches/abstract_vars/theories/itt/itt_dprod.mli
+4 -25 metaprl-branches/abstract_vars/theories/itt/itt_equal.ml
+2 -1 metaprl-branches/abstract_vars/theories/itt/itt_equal.mli
+3 -2 metaprl-branches/abstract_vars/theories/itt/itt_int_base.mli
+3 -2 metaprl-branches/abstract_vars/theories/itt/itt_isect.mli
+17 -35 metaprl-branches/abstract_vars/theories/itt/itt_list.ml
+3 -2 metaprl-branches/abstract_vars/theories/itt/itt_list.mli
+35 -69 metaprl-branches/abstract_vars/theories/itt/itt_logic.ml
+5 -4 metaprl-branches/abstract_vars/theories/itt/itt_logic.mli
+12 -30 metaprl-branches/abstract_vars/theories/itt/itt_prec.ml
+9 -8 metaprl-branches/abstract_vars/theories/itt/itt_prec.mli
+3 -2 metaprl-branches/abstract_vars/theories/itt/itt_quotient.mli
+18 -41 metaprl-branches/abstract_vars/theories/itt/itt_rfun.ml
+11 -10 metaprl-branches/abstract_vars/theories/itt/itt_rfun.mli
+3 -2 metaprl-branches/abstract_vars/theories/itt/itt_set.mli
+14 -30 metaprl-branches/abstract_vars/theories/itt/itt_srec.ml
+5 -4 metaprl-branches/abstract_vars/theories/itt/itt_srec.mli
+15 -40 metaprl-branches/abstract_vars/theories/itt/itt_struct2.ml
+3 -0 metaprl-branches/abstract_vars/theories/itt/itt_struct3.mli
+17 -37 metaprl-branches/abstract_vars/theories/itt/itt_union.ml
+3 -2 metaprl-branches/abstract_vars/theories/itt/itt_union.mli
+13 -31 metaprl-branches/abstract_vars/theories/itt/itt_w.ml
+5 -4 metaprl-branches/abstract_vars/theories/itt/itt_w.mli
+2 -2 mpcompiler-branches/abstract_vars/mmc/core/core_test.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-06 21:11:26 -0700 (Sun, 06 Jul 2003)
Revision: 4706
Log message:

      Migrated String_util and Mp_debug to libmojave versions.
      

Changes  Path
+1 -1 metaprl-branches/abstract_vars/editor/ml/mp.ml
+1 -1 metaprl-branches/abstract_vars/editor/ml/mp_top.ml
+1 -1 metaprl-branches/abstract_vars/editor/ml/nuprl_eval.ml
+1 -1 metaprl-branches/abstract_vars/editor/ml/nuprl_run.ml
+1 -1 metaprl-branches/abstract_vars/editor/ml/shell_http.ml
+1 -1 metaprl-branches/abstract_vars/editor/ml/shell_mp.ml
+1 -1 metaprl-branches/abstract_vars/editor/ml/shell_p4.ml
+1 -1 metaprl-branches/abstract_vars/editor/ml/tests/czf.ml
+2 -2 metaprl-branches/abstract_vars/editor/ml/tests/prop-pigeon.ml
+1 -1 metaprl-branches/abstract_vars/editor/ml/tests/seq_addrs_test.ml
+1 -1 metaprl-branches/abstract_vars/editor/ml/tutorial.ml
+1 -1 metaprl-branches/abstract_vars/editor/ml/tutorial_itt.ml
+1 -1 metaprl-branches/abstract_vars/ensemble/appl_closure.ml
+1 -1 metaprl-branches/abstract_vars/ensemble/appl_outboard_client.ml
+1 -1 metaprl-branches/abstract_vars/ensemble/appl_outboard_server.ml
+1 -1 metaprl-branches/abstract_vars/ensemble/ensemble_queue.ml
+1 -1 metaprl-branches/abstract_vars/ensemble/remote_ensemble.ml
+1 -1 metaprl-branches/abstract_vars/ensemble/remote_monitor.ml
+1 -1 metaprl-branches/abstract_vars/ensemble/thread_refiner_ens.ml
+4 -3 metaprl-branches/abstract_vars/filter/OMakefile
+3 -3 metaprl-branches/abstract_vars/filter/base/filter_ast.ml
+3 -3 metaprl-branches/abstract_vars/filter/base/filter_buffer.ml
+3 -3 metaprl-branches/abstract_vars/filter/base/filter_cache.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/filter_cache_fun.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/filter_comment.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/filter_exn.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/filter_grammar.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/filter_hash.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/filter_ocaml.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/filter_spell.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/filter_summary.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/filter_summary_io.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/filter_summary_util.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/filter_util.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/free_vars.ml
+1 -1 metaprl-branches/abstract_vars/filter/base/mLast_util.ml
+1 -1 metaprl-branches/abstract_vars/filter/boot/conversionals_boot.ml
+1 -1 metaprl-branches/abstract_vars/filter/boot/proof_boot.ml
+1 -1 metaprl-branches/abstract_vars/filter/boot/proof_convert.ml
+1 -1 metaprl-branches/abstract_vars/filter/boot/proof_term_boot.ml
+1 -1 metaprl-branches/abstract_vars/filter/boot/rewrite_boot.ml
+1 -1 metaprl-branches/abstract_vars/filter/boot/sequent_boot.ml
+1 -1 metaprl-branches/abstract_vars/filter/boot/tactic_boot.ml
+1 -1 metaprl-branches/abstract_vars/filter/boot/tacticals_boot.ml
+1 -1 metaprl-branches/abstract_vars/filter/filter/filter_bin.ml
+1 -1 metaprl-branches/abstract_vars/filter/filter/filter_convert.ml
+2 -2 metaprl-branches/abstract_vars/filter/filter/filter_main.ml
+1 -1 metaprl-branches/abstract_vars/filter/filter/filter_parse.ml
+1 -1 metaprl-branches/abstract_vars/filter/filter/filter_patt.ml
+3 -3 metaprl-branches/abstract_vars/filter/filter/filter_prog.ml
+2 -2 metaprl-branches/abstract_vars/filter/filter/prlcomp.ml
+1 -1 metaprl-branches/abstract_vars/filter/filter/term_grammar.ml
+1 -1 metaprl-branches/abstract_vars/filter/phobos/filter_phobos.ml
+1 -1 metaprl-branches/abstract_vars/filter/phobos/phobos_compile.ml
+1 -1 metaprl-branches/abstract_vars/filter/phobos/phobos_debug.ml
+1 -1 metaprl-branches/abstract_vars/filter/phobos/phobos_main.ml
+1 -1 metaprl-branches/abstract_vars/filter/phobos/phobos_rewrite.ml
+1 -1 metaprl-branches/abstract_vars/filter/phobos/phobos_state.ml
+4 -4 metaprl-branches/abstract_vars/library/ascii_scan.ml
+1 -1 metaprl-branches/abstract_vars/library/basic.ml
+1 -1 metaprl-branches/abstract_vars/library/bigInt.ml
+8 -8 metaprl-branches/abstract_vars/library/db.ml
+1 -1 metaprl-branches/abstract_vars/library/definition.ml
+1 -1 metaprl-branches/abstract_vars/library/library.ml
+2 -2 metaprl-branches/abstract_vars/library/library_type_base.ml
+1 -1 metaprl-branches/abstract_vars/library/link.ml
+1 -1 metaprl-branches/abstract_vars/library/lint32.ml
+16 -16 metaprl-branches/abstract_vars/library/mathBus.ml
+1 -1 metaprl-branches/abstract_vars/library/mbterm.ml
+1 -1 metaprl-branches/abstract_vars/library/nuprl5.ml
+1 -1 metaprl-branches/abstract_vars/library/object_id.ml
+1 -1 metaprl-branches/abstract_vars/library/oidtable.ml
+1 -1 metaprl-branches/abstract_vars/library/orb.ml
+6 -6 metaprl-branches/abstract_vars/library/registry.ml
+1 -1 metaprl-branches/abstract_vars/library/socketIo.ml
+1 -1 metaprl-branches/abstract_vars/library/tentfunctor.ml
+1 -1 metaprl-branches/abstract_vars/library/test.ml
+1 -1 metaprl-branches/abstract_vars/library/utils.ml
+0 -3 metaprl-branches/abstract_vars/mllib/Makefile
+3 -3 metaprl-branches/abstract_vars/mllib/OMakefile
+1 -1 metaprl-branches/abstract_vars/mllib/array_util.ml
+1 -1 metaprl-branches/abstract_vars/mllib/bitset.ml
+1 -1 metaprl-branches/abstract_vars/mllib/debug_string_sets.ml
+3 -3 metaprl-branches/abstract_vars/mllib/env_arg.ml
+1 -1 metaprl-branches/abstract_vars/mllib/file_base.ml
+1 -1 metaprl-branches/abstract_vars/mllib/file_type_base.ml
+2 -2 metaprl-branches/abstract_vars/mllib/file_util.ml
+8 -8 metaprl-branches/abstract_vars/mllib/filename_util.ml
+6 -6 metaprl-branches/abstract_vars/mllib/http_server.ml
+1 -1 metaprl-branches/abstract_vars/mllib/imp_dag.ml
+1 -1 metaprl-branches/abstract_vars/mllib/list_util.ml
+1 -1 metaprl-branches/abstract_vars/mllib/memo.ml
+1 -1 metaprl-branches/abstract_vars/mllib/mmap_pipe.ml
Deleted metaprl-branches/abstract_vars/mllib/mp_debug.ml
Deleted metaprl-branches/abstract_vars/mllib/mp_debug.mli
+1 -1 metaprl-branches/abstract_vars/mllib/mp_inet.ml
+1 -1 metaprl-branches/abstract_vars/mllib/mp_pervasives.ml
+1 -1 metaprl-branches/abstract_vars/mllib/mp_term.ml
+1 -1 metaprl-branches/abstract_vars/mllib/precedence.ml
+1 -1 metaprl-branches/abstract_vars/mllib/ref_util.ml
+1 -1 metaprl-branches/abstract_vars/mllib/remote_queue_null.ml
Deleted metaprl-branches/abstract_vars/mllib/string_set.ml
Deleted metaprl-branches/abstract_vars/mllib/string_set.mli
Deleted metaprl-branches/abstract_vars/mllib/string_util.ml
Deleted metaprl-branches/abstract_vars/mllib/string_util.mli
+1 -1 metaprl-branches/abstract_vars/mllib/thread_event.ml
+3 -1 metaprl-branches/abstract_vars/refiner/refbase/OMakefile
+1 -1 metaprl-branches/abstract_vars/refiner/refbase/opname.ml
+1 -1 metaprl-branches/abstract_vars/refiner/refiner/refine.ml
+7 -7 metaprl-branches/abstract_vars/refiner/reflib/ascii_io.ml
+2 -2 metaprl-branches/abstract_vars/refiner/reflib/ascii_io_sig.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/dform.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/dform_print.ml
+3 -3 metaprl-branches/abstract_vars/refiner/reflib/jall.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/match_seq.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/ml_file.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/ml_format.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/ml_print.ml
+3 -3 metaprl-branches/abstract_vars/refiner/reflib/ml_string.ml
+2 -2 metaprl-branches/abstract_vars/refiner/reflib/mp_resource.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/refine_exn.ml
+4 -4 metaprl-branches/abstract_vars/refiner/reflib/rformat.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/simple_print.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/term_compare.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/term_dtable.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/term_match_table.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/term_stable.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/theory.ml
+1 -1 metaprl-branches/abstract_vars/refiner/reflib/unify_mm.ml
+1 -1 metaprl-branches/abstract_vars/refiner/rewrite/rewrite.ml
+2 -2 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_build_contractum.ml
+1 -1 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_compile_contractum.ml
+2 -2 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_compile_redex.ml
+1 -1 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_debug.ml
+1 -1 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_match_redex.ml
+1 -1 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_meta.ml
+1 -1 metaprl-branches/abstract_vars/refiner/rewrite/rewrite_util.ml
+2 -2 metaprl-branches/abstract_vars/refiner/term_ds/rob_ds.ml
+1 -1 metaprl-branches/abstract_vars/refiner/term_ds/rob_ds.mli
+1 -1 metaprl-branches/abstract_vars/refiner/term_ds/term_addr_ds.ml
+1 -1 metaprl-branches/abstract_vars/refiner/term_ds/term_base_ds.ml
+1 -1 metaprl-branches/abstract_vars/refiner/term_ds/term_ds.ml
+1 -1 metaprl-branches/abstract_vars/refiner/term_ds/term_man_ds.ml
+1 -1 metaprl-branches/abstract_vars/refiner/term_ds/term_subst_ds.ml
+1 -1 metaprl-branches/abstract_vars/refiner/term_gen/term_addr_gen.ml
+2 -2 metaprl-branches/abstract_vars/refiner/term_gen/term_header_constr.ml
+1 -1 metaprl-branches/abstract_vars/refiner/term_gen/term_man_gen.ml
+1 -1 metaprl-branches/abstract_vars/refiner/term_std/term_base_std.ml
+1 -1 metaprl-branches/abstract_vars/refiner/term_std/term_std.ml
+1 -1 metaprl-branches/abstract_vars/refiner/term_std/term_subst_std.ml
+4 -4 metaprl-branches/abstract_vars/support/display/base_dform.ml
+3 -3 metaprl-branches/abstract_vars/support/display/nuprl_font.ml
+1 -1 metaprl-branches/abstract_vars/support/display/ocaml_base_df.ml
+1 -1 metaprl-branches/abstract_vars/support/display/ocaml_expr_df.ml
+1 -1 metaprl-branches/abstract_vars/support/display/ocaml_me_df.ml
+1 -1 metaprl-branches/abstract_vars/support/display/ocaml_mt_df.ml
+1 -1 metaprl-branches/abstract_vars/support/display/ocaml_patt_df.ml
+1 -1 metaprl-branches/abstract_vars/support/display/ocaml_sig_df.ml
+1 -1 metaprl-branches/abstract_vars/support/display/ocaml_str_df.ml
+1 -1 metaprl-branches/abstract_vars/support/display/ocaml_type_df.ml
+2 -2 metaprl-branches/abstract_vars/support/display/perv.ml
+1 -1 metaprl-branches/abstract_vars/support/display/summary.ml
+1 -1 metaprl-branches/abstract_vars/support/shell/display_term.ml
+2 -2 metaprl-branches/abstract_vars/support/shell/mux_channel.ml
+2 -2 metaprl-branches/abstract_vars/support/shell/package_info.ml
+1 -1 metaprl-branches/abstract_vars/support/shell/proof_edit.ml
+4 -5 metaprl-branches/abstract_vars/support/shell/shell.ml
+1 -1 metaprl-branches/abstract_vars/support/shell/shell_rewrite.ml
+1 -1 metaprl-branches/abstract_vars/support/shell/shell_root.ml
+1 -1 metaprl-branches/abstract_vars/support/shell/shell_rule.ml
+5 -5 metaprl-branches/abstract_vars/support/shell/shell_state.ml
+2 -2 metaprl-branches/abstract_vars/support/tactics/auto_tactic.ml
+1 -1 metaprl-branches/abstract_vars/support/tactics/dtactic.ml
+1 -1 metaprl-branches/abstract_vars/support/tactics/simp_typeinf.ml
+1 -1 metaprl-branches/abstract_vars/support/tactics/tactic_cache.ml
+1 -1 metaprl-branches/abstract_vars/support/tactics/top_conversionals.ml
+1 -1 metaprl-branches/abstract_vars/support/tactics/typeinf.ml
+2 -2 metaprl-branches/abstract_vars/support/tactics/var.ml
+1 -1 metaprl-branches/abstract_vars/theories/base/base_rewrite.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_abel_group.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_abel_group.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_all.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_and.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_axioms.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_bool.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_coset.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_coset.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_cyclic_group.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_cyclic_group.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_cyclic_subgroup.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_cyclic_subgroup.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_dall.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_dexists.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_empty.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_equiv.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_equiv.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_exists.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_false.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_group.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_group.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_group_bvd.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_group_bvd.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_group_power.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_group_power.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_hom.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_hom.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_implies.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_inv_image.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_inv_image.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_isect.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_iso.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_iso.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_ker.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_ker.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_kleingroup.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_kleingroup.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_normal_subgroup.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_normal_subgroup.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_or.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_sall.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_sep.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_set.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_set_bvd.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_set_bvd.mli
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_set_ind.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_setdiff.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_sexists.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_singleton.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_subgroup.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_true.ml
+1 -1 metaprl-branches/abstract_vars/theories/czf/czf_itt_union.ml
+1 -1 metaprl-branches/abstract_vars/theories/experimental/compile/m_closure.ml
+1 -1 metaprl-branches/abstract_vars/theories/experimental/compile/m_cps.ml
+1 -1 metaprl-branches/abstract_vars/theories/experimental/compile/m_post_parsing.ml
+1 -1 metaprl-branches/abstract_vars/theories/experimental/compile/m_prog.ml
+1 -1 metaprl-branches/abstract_vars/theories/experimental/compile/m_standardize.ml
+1 -1 metaprl-branches/abstract_vars/theories/experimental/compile/m_util.ml
+1 -1 metaprl-branches/abstract_vars/theories/experimental/compile/m_x86_regalloc.ml
+1 -1 metaprl-branches/abstract_vars/theories/experimental/compile/m_x86_spill.ml
+1 -1 metaprl-branches/abstract_vars/theories/experimental/compile/m_x86_term.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/ctt_markov.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_algebra_df.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_atom.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_bintree.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_bintree.mli
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_bisect.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_bunion.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_collection.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_collection.mli
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_cyclic_group.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_cyclic_group.mli
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_datatree.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_decidable.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_dfun.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_disect.ml
+2 -2 metaprl-branches/abstract_vars/theories/itt/itt_dprod.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_dprod_imp.ml
+2 -2 metaprl-branches/abstract_vars/theories/itt/itt_equal.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_ext_equal.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_fset.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_fun.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_group.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_group.mli
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_grouplikeobj.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_grouplikeobj.mli
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_int_arith.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_int_base.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_int_ext.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_inv_typing.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_inv_typing.mli
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_isect.ml
+2 -2 metaprl-branches/abstract_vars/theories/itt/itt_list.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_logic.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_nat.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_pointwise.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_pointwise2.ml
+2 -2 metaprl-branches/abstract_vars/theories/itt/itt_prec.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_prod.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_prop_decide.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_quotient.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_quotient_group.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_quotient_group.mli
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_rbtree.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_record.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_record0.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_record_exm.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_record_label.ml
+2 -2 metaprl-branches/abstract_vars/theories/itt/itt_rfun.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_set.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_singleton.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_sortedtree.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_squash.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_squiggle.ml
+2 -2 metaprl-branches/abstract_vars/theories/itt/itt_srec.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_struct.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_struct2.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_struct3.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_struct3.mli
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_subset.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_subset2.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_subtype.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_test.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_tsquash.ml
+2 -2 metaprl-branches/abstract_vars/theories/itt/itt_union.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_unit.ml
+1 -1 metaprl-branches/abstract_vars/theories/itt/itt_void.ml
+1 -1 metaprl-branches/abstract_vars/theories/lf/main.ml
+1 -1 metaprl-branches/abstract_vars/theories/ocaml_sos/ocaml_expr_sos.ml
+1 -1 metaprl-branches/abstract_vars/theories/ocaml_sos/ocaml_logic.ml
+1 -1 metaprl-branches/abstract_vars/theories/ocaml_sos/ocaml_me_sos.ml
+1 -1 metaprl-branches/abstract_vars/theories/ocaml_sos/ocaml_mt_sos.ml
+1 -1 metaprl-branches/abstract_vars/theories/ocaml_sos/ocaml_patt_sos.ml
+1 -1 metaprl-branches/abstract_vars/theories/ocaml_sos/ocaml_sig_sos.ml
+1 -1 metaprl-branches/abstract_vars/theories/ocaml_sos/ocaml_str_sos.ml
+1 -1 metaprl-branches/abstract_vars/theories/ocaml_sos/ocaml_type_sos.ml
+1 -1 metaprl-branches/abstract_vars/theories/tptp/tptp.ml
+2 -2 metaprl-branches/abstract_vars/theories/tptp/tptp_cache.ml
+1 -1 metaprl-branches/abstract_vars/theories/tptp/tptp_cache.mli
+1 -1 metaprl-branches/abstract_vars/theories/tptp/tptp_lex.mll
+2 -2 metaprl-branches/abstract_vars/theories/tptp/tptp_load.ml
+2 -2 metaprl-branches/abstract_vars/theories/tptp/tptp_prove.ml
+1 -1 metaprl-branches/abstract_vars/util/ocamldep.mll
+1 -1 mpcompiler-branches/abstract_vars/mmc/core/mmc_core_util.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2003-07-09 00:20:04 -0700 (Wed, 09 Jul 2003)
Revision: 4723
Log message:

      Merging in the abstract_vars branch:
      - variables are now an abstract type, not strings
      - MVar parameters are gone
      
      See the branch log messages for more information.
      
      P.S. This is a pretty big change, so I bumped the version number
      in mk/preface.
      

Changes  Path
+8 -4 metaprl/Makefile
+46 -49 metaprl/OMakefile
+0 -3 metaprl/clib/Makefile
+0 -3 metaprl/clib/OMakefile
Deleted metaprl/clib/getrusage.c
Deleted metaprl/clib/mmap.c
Deleted metaprl/clib/mmap.h
Deleted metaprl/clib/readline.c
+6 -9 metaprl/editor/ml/Makefile
+5 -9 metaprl/editor/ml/OMakefile
+1 -1 metaprl/editor/ml/mp.ml
+1 -1 metaprl/editor/ml/mp_top.ml
+30 -58 metaprl/editor/ml/nuprl_eval.ml
+8 -3 metaprl/editor/ml/nuprl_jprover.ml
+1 -1 metaprl/editor/ml/nuprl_run.ml
+2 -2 metaprl/editor/ml/shell_http.ml
+3 -3 metaprl/editor/ml/shell_mp.ml
+3 -3 metaprl/editor/ml/shell_p4.ml
+1 -1 metaprl/editor/ml/tests/czf.ml
+2 -2 metaprl/editor/ml/tests/prop-pigeon.ml
+1 -1 metaprl/editor/ml/tests/seq_addrs_test.ml
+1 -1 metaprl/editor/ml/tutorial.ml
+1 -1 metaprl/editor/ml/tutorial_itt.ml
+2 -2 metaprl/ensemble/appl_closure.ml
+10 -10 metaprl/ensemble/appl_outboard_client.ml
+11 -11 metaprl/ensemble/appl_outboard_server.ml
+9 -9 metaprl/ensemble/ensemble_queue.ml
+11 -11 metaprl/ensemble/remote_ensemble.ml
+2 -2 metaprl/ensemble/remote_monitor.ml
+3 -3 metaprl/ensemble/remote_null.ml
+1 -1 metaprl/ensemble/remote_sig.mlz
+26 -26 metaprl/ensemble/thread_refiner_ens.ml
+8 -4 metaprl/filter/Makefile
+6 -3 metaprl/filter/OMakefile
+4 -4 metaprl/filter/base/filter_ast.ml
+3 -3 metaprl/filter/base/filter_buffer.ml
+11 -7 metaprl/filter/base/filter_cache.ml
+5 -5 metaprl/filter/base/filter_cache_fun.ml
+2 -2 metaprl/filter/base/filter_comment.ml
+1 -1 metaprl/filter/base/filter_exn.ml
+1 -1 metaprl/filter/base/filter_grammar.ml
+1 -1 metaprl/filter/base/filter_hash.ml
+1 -1 metaprl/filter/base/filter_magic.ml
+34 -32 metaprl/filter/base/filter_ocaml.ml
+2 -2 metaprl/filter/base/filter_ocaml.mli
+1 -1 metaprl/filter/base/filter_spell.ml
+45 -44 metaprl/filter/base/filter_summary.ml
+1 -0 metaprl/filter/base/filter_summary.mli
+3 -3 metaprl/filter/base/filter_summary_io.ml
+1 -1 metaprl/filter/base/filter_summary_util.ml
+4 -3 metaprl/filter/base/filter_summary_util.mli
+14 -12 metaprl/filter/base/filter_type.ml
+5 -5 metaprl/filter/base/filter_util.ml
+3 -2 metaprl/filter/base/filter_util.mli
+1 -1 metaprl/filter/base/free_vars.ml
+1 -1 metaprl/filter/base/mLast_util.ml
+1 -0 metaprl/filter/boot/OMakefile
+1 -1 metaprl/filter/boot/conversionals_boot.ml
+12 -12 metaprl/filter/boot/proof_boot.ml
+1 -1 metaprl/filter/boot/proof_convert.ml
+7 -7 metaprl/filter/boot/proof_term_boot.ml
+1 -1 metaprl/filter/boot/rewrite_boot.ml
+1 -1 metaprl/filter/boot/sequent_boot.ml
+17 -17 metaprl/filter/boot/tactic_boot.ml
+14 -15 metaprl/filter/boot/tactic_boot_sig.mlz
+1 -1 metaprl/filter/boot/tacticals_boot.ml
+1 -1 metaprl/filter/filter/filter_bin.ml
+1 -1 metaprl/filter/filter/filter_convert.ml
+2 -2 metaprl/filter/filter/filter_main.ml
+17 -14 metaprl/filter/filter/filter_parse.ml
+20 -17 metaprl/filter/filter/filter_patt.ml
+34 -25 metaprl/filter/filter/filter_prog.ml
+2 -2 metaprl/filter/filter/prlcomp.ml
+50 -58 metaprl/filter/filter/term_grammar.ml
+1 -0 metaprl/filter/phobos/OMakefile
+1 -1 metaprl/filter/phobos/filter_phobos.ml
+1 -1 metaprl/filter/phobos/phobos_compile.ml
+1 -1 metaprl/filter/phobos/phobos_debug.ml
+1 -1 metaprl/filter/phobos/phobos_main.ml
+9 -11 metaprl/filter/phobos/phobos_parser.mly
+9 -9 metaprl/filter/phobos/phobos_rewrite.ml
+1 -1 metaprl/filter/phobos/phobos_state.ml
+3 -0 metaprl/library/OMakefile
+5 -5 metaprl/library/ascii_scan.ml
+1 -1 metaprl/library/ascii_scan.mli
+14 -14 metaprl/library/basic.ml
+1 -1 metaprl/library/basic.mli
+1 -1 metaprl/library/bigInt.ml
+39 -26 metaprl/library/db.ml
+1 -1 metaprl/library/definition.ml
+1 -1 metaprl/library/library.ml
+2 -2 metaprl/library/library_type_base.ml
+3 -3 metaprl/library/link.ml
+1 -1 metaprl/library/lint32.ml
+23 -23 metaprl/library/mathBus.ml
+1 -1 metaprl/library/mathBus.mli
+22 -27 metaprl/library/mbterm.ml
+5 -5 metaprl/library/nuprl5.ml
+9 -8 metaprl/library/nuprl5.mli
+1 -1 metaprl/library/object_id.ml
+1 -1 metaprl/library/oidtable.ml
+3 -3 metaprl/library/orb.ml
+7 -7 metaprl/library/registry.ml
+1 -1 metaprl/library/socketIo.ml
+1 -1 metaprl/library/tentfunctor.ml
+1 -1 metaprl/library/test.ml
+1 -1 metaprl/library/utils.ml
+1 -1 metaprl/mk/preface
Added metaprl/mllib/Files
Properties metaprl/mllib/Files
+3 -73 metaprl/mllib/Makefile
+6 -74 metaprl/mllib/OMakefile
+3 -3 metaprl/mllib/array_linear_set.ml
Deleted metaprl/mllib/array_util.ml
Deleted metaprl/mllib/array_util.mli
+1 -1 metaprl/mllib/bitset.ml
+1 -1 metaprl/mllib/debug_string_sets.ml
+3 -3 metaprl/mllib/env_arg.ml
+1 -1 metaprl/mllib/file_base.ml
+4 -4 metaprl/mllib/file_type_base.ml
Deleted metaprl/mllib/file_util.ml
Deleted metaprl/mllib/file_util.mli
Deleted metaprl/mllib/filename_util.ml
Deleted metaprl/mllib/filename_util.mli
Deleted metaprl/mllib/getrusage.ml
Deleted metaprl/mllib/getrusage.mli
Deleted metaprl/mllib/hashtbl_util.ml
Deleted metaprl/mllib/hashtbl_util.mli
+14 -14 metaprl/mllib/http_server.ml
+1 -1 metaprl/mllib/http_server.mli
+1 -1 metaprl/mllib/imp_dag.ml
Deleted metaprl/mllib/int_util.ml
Deleted metaprl/mllib/int_util.mli
+2 -2 metaprl/mllib/large_array.ml
+2 -2 metaprl/mllib/large_weak_array.ml
+1 -1 metaprl/mllib/linear_set.mlz
Deleted metaprl/mllib/list_util.ml
Deleted metaprl/mllib/list_util.mli
+4 -4 metaprl/mllib/marshal_shared.ml
+1 -1 metaprl/mllib/memo.ml
Deleted metaprl/mllib/mmap.ml
Deleted metaprl/mllib/mmap.mli
Deleted metaprl/mllib/mmap_pipe.ml
Deleted metaprl/mllib/mmap_pipe.mli
Deleted metaprl/mllib/mp_big_int.ml
Deleted metaprl/mllib/mp_big_int.mli
Deleted metaprl/mllib/mp_debug.ml
Deleted metaprl/mllib/mp_debug.mli
Deleted metaprl/mllib/mp_id.ml
Deleted metaprl/mllib/mp_id.mli
Deleted metaprl/mllib/mp_inet.ml
Deleted metaprl/mllib/mp_inet.mli
Deleted metaprl/mllib/mp_num.ml
Deleted metaprl/mllib/mp_num.mli
Deleted metaprl/mllib/mp_pervasives.ml
Deleted metaprl/mllib/mp_pervasives.mli
+1 -1 metaprl/mllib/mp_term.ml
+1 -1 metaprl/mllib/precedence.ml
Deleted metaprl/mllib/readline.ml
Deleted metaprl/mllib/readline.mli
+1 -1 metaprl/mllib/red_black_set.ml
Deleted metaprl/mllib/ref_util.ml
Deleted metaprl/mllib/ref_util.mli
+1 -1 metaprl/mllib/remote_lazy_queue_sig.ml
+10 -10 metaprl/mllib/remote_queue_null.ml
+1 -1 metaprl/mllib/remote_queue_sig.ml
+1 -1 metaprl/mllib/set_sig.mlz
+4 -4 metaprl/mllib/small_set.ml
+1 -1 metaprl/mllib/splay_linear_set.ml
Deleted metaprl/mllib/string_set.ml
Deleted metaprl/mllib/string_set.mli
Deleted metaprl/mllib/string_util.ml
Deleted metaprl/mllib/string_util.mli
Deleted metaprl/mllib/thread_event.ml
Deleted metaprl/mllib/thread_event.mli
Deleted metaprl/mllib/thread_util.ml
Deleted metaprl/mllib/thread_util.mli
Deleted metaprl/mllib/unix_util.ml
Deleted metaprl/mllib/unix_util.mli
+3 -1 metaprl/refiner/refbase/OMakefile
+2 -2 metaprl/refiner/refbase/opname.ml
+3 -2 metaprl/refiner/refiner/OMakefile
+27 -27 metaprl/refiner/refiner/refine.ml
+22 -11 metaprl/refiner/refiner/refine_error.ml
+3 -2 metaprl/refiner/reflib/OMakefile
+1 -1 metaprl/refiner/reflib/arith.ml
+29 -28 metaprl/refiner/reflib/ascii_io.ml
+2 -2 metaprl/refiner/reflib/ascii_io_sig.ml
+65 -47 metaprl/refiner/reflib/dform.ml
+3 -3 metaprl/refiner/reflib/dform_print.ml
+26 -3 metaprl/refiner/reflib/jall.ml
+2 -2 metaprl/refiner/reflib/match_seq.ml
+1 -1 metaprl/refiner/reflib/ml_file.ml
+17 -10 metaprl/refiner/reflib/ml_format.ml
+5 -5 metaprl/refiner/reflib/ml_format_sig.mlz
+2 -2 metaprl/refiner/reflib/ml_print.ml
+3 -3 metaprl/refiner/reflib/ml_string.ml
+1 -1 metaprl/refiner/reflib/ml_term.ml
+2 -2 metaprl/refiner/reflib/ml_term.mli
+8 -7 metaprl/refiner/reflib/mp_resource.ml
+2 -1 metaprl/refiner/reflib/mp_resource.mli
+17 -12 metaprl/refiner/reflib/refine_exn.ml
+5 -5 metaprl/refiner/reflib/rformat.ml
+1 -1 metaprl/refiner/reflib/rformat.mli
+21 -17 metaprl/refiner/reflib/simple_print.ml
+3 -4 metaprl/refiner/reflib/term_compare.ml
+1 -1 metaprl/refiner/reflib/term_dtable.ml
+4 -3 metaprl/refiner/reflib/term_match_table.ml
+1 -1 metaprl/refiner/reflib/term_stable.ml
+2 -2 metaprl/refiner/reflib/theory.ml
+26 -25 metaprl/refiner/reflib/unify_mm.ml
+10 -10 metaprl/refiner/reflib/unify_mm.mli
+3 -2 metaprl/refiner/refsig/OMakefile
+11 -9 metaprl/refiner/refsig/refine_error_sig.ml
+10 -10 metaprl/refiner/refsig/refine_sig.ml
+19 -14 metaprl/refiner/refsig/rewrite_sig.ml
+6 -6 metaprl/refiner/refsig/term_addr_sig.ml
+9 -8 metaprl/refiner/refsig/term_base_sig.ml
+12 -11 metaprl/refiner/refsig/term_eval_sig.ml
+4 -28 metaprl/refiner/refsig/term_hash_sig.ml
+8 -8 metaprl/refiner/refsig/term_man_sig.ml
+3 -2 metaprl/refiner/refsig/term_meta_sig.ml
+47 -45 metaprl/refiner/refsig/term_op_sig.ml
+12 -12 metaprl/refiner/refsig/term_sig.ml
+19 -19 metaprl/refiner/refsig/term_subst_sig.ml
+3 -2 metaprl/refiner/rewrite/OMakefile
+42 -37 metaprl/refiner/rewrite/rewrite.ml
+58 -43 metaprl/refiner/rewrite/rewrite_build_contractum.ml
+3 -2 metaprl/refiner/rewrite/rewrite_build_contractum.mli
+14 -15 metaprl/refiner/rewrite/rewrite_compile_contractum.ml
+3 -2 metaprl/refiner/rewrite/rewrite_compile_contractum.mli
+26 -26 metaprl/refiner/rewrite/rewrite_compile_redex.ml
+2 -1 metaprl/refiner/rewrite/rewrite_compile_redex.mli
+29 -26 metaprl/refiner/rewrite/rewrite_debug.ml
+45 -45 metaprl/refiner/rewrite/rewrite_match_redex.ml
+2 -2 metaprl/refiner/rewrite/rewrite_match_redex.mli
+10 -13 metaprl/refiner/rewrite/rewrite_meta.ml
+16 -16 metaprl/refiner/rewrite/rewrite_types.ml
+16 -16 metaprl/refiner/rewrite/rewrite_util.ml
+28 -27 metaprl/refiner/rewrite/rewrite_util_sig.ml
+2 -2 metaprl/refiner/term_ds/OMakefile
+2 -2 metaprl/refiner/term_ds/rob_ds.ml
+1 -1 metaprl/refiner/term_ds/rob_ds.mli
+5 -6 metaprl/refiner/term_ds/term_addr_ds.ml
+37 -39 metaprl/refiner/term_ds/term_base_ds.ml
+16 -17 metaprl/refiner/term_ds/term_ds.ml
+27 -28 metaprl/refiner/term_ds/term_ds_sig.ml
+6 -6 metaprl/refiner/term_ds/term_eval_ds.ml
+8 -8 metaprl/refiner/term_ds/term_man_ds.ml
+5 -5 metaprl/refiner/term_ds/term_op_ds.ml
+58 -57 metaprl/refiner/term_ds/term_subst_ds.ml
+3 -2 metaprl/refiner/term_gen/OMakefile
+6 -8 metaprl/refiner/term_gen/term_addr_gen.ml
+10 -9 metaprl/refiner/term_gen/term_hash.ml
+2 -3 metaprl/refiner/term_gen/term_header_constr.ml
+17 -17 metaprl/refiner/term_gen/term_man_gen.ml
+2 -2 metaprl/refiner/term_gen/term_meta_gen.ml
+1 -1 metaprl/refiner/term_gen/term_shape_gen.ml
+2 -2 metaprl/refiner/term_std/OMakefile
+3 -4 metaprl/refiner/term_std/term_base_std.ml
+4 -4 metaprl/refiner/term_std/term_eval_std.ml
+13 -13 metaprl/refiner/term_std/term_std.ml
+20 -20 metaprl/refiner/term_std/term_std_sig.ml
+40 -39 metaprl/refiner/term_std/term_subst_std.ml
+26 -35 metaprl/support/display/base_dform.ml
+1 -1 metaprl/support/display/base_dform.mli
+3 -3 metaprl/support/display/nuprl_font.ml
+1 -1 metaprl/support/display/ocaml_base_df.ml
+1 -1 metaprl/support/display/ocaml_expr_df.ml
+1 -1 metaprl/support/display/ocaml_me_df.ml
+1 -1 metaprl/support/display/ocaml_mt_df.ml
+1 -1 metaprl/support/display/ocaml_patt_df.ml
+1 -1 metaprl/support/display/ocaml_sig_df.ml
+1 -1 metaprl/support/display/ocaml_str_df.ml
+1 -1 metaprl/support/display/ocaml_type_df.ml
+2 -2 metaprl/support/display/perv.ml
+5 -4 metaprl/support/display/perv.mli
+19 -17 metaprl/support/display/summary.ml
+7 -9 metaprl/support/display/summary.mli
+1 -1 metaprl/support/shell/display_term.ml
+2 -2 metaprl/support/shell/mptop.ml
+2 -2 metaprl/support/shell/mux_channel.ml
+2 -2 metaprl/support/shell/package_info.ml
+6 -6 metaprl/support/shell/proof_edit.ml
+5 -6 metaprl/support/shell/shell.ml
+12 -12 metaprl/support/shell/shell_package.ml
+2 -2 metaprl/support/shell/shell_rewrite.ml
+1 -1 metaprl/support/shell/shell_root.ml
+1 -1 metaprl/support/shell/shell_rule.ml
+17 -10 metaprl/support/shell/shell_state.ml
+1 -1 metaprl/support/shell/shell_state.mli
+2 -2 metaprl/support/tactics/auto_tactic.ml
+1 -1 metaprl/support/tactics/dtactic.ml
+7 -11 metaprl/support/tactics/simp_typeinf.ml
+3 -3 metaprl/support/tactics/simp_typeinf.mli
+30 -29 metaprl/support/tactics/tactic_cache.ml
+3 -2 metaprl/support/tactics/tactic_cache.mli
+1 -1 metaprl/support/tactics/top_conversionals.ml
+13 -68 metaprl/support/tactics/top_tacticals.ml
+10 -10 metaprl/support/tactics/typeinf.ml
+5 -5 metaprl/support/tactics/typeinf.mli
+13 -44 metaprl/support/tactics/var.ml
+5 -4 metaprl/support/tactics/var.mli
+10 -13 metaprl/theories/base/base_meta.ml
+0 -2 metaprl/theories/base/base_meta.mli
+2 -2 metaprl/theories/base/base_rewrite.ml
+1 -1 metaprl/theories/czf/czf_itt_abel_group.ml
+1 -1 metaprl/theories/czf/czf_itt_abel_group.mli
+1 -1 metaprl/theories/czf/czf_itt_all.ml
+1 -1 metaprl/theories/czf/czf_itt_and.ml
+1 -1 metaprl/theories/czf/czf_itt_axioms.ml
+1 -1 metaprl/theories/czf/czf_itt_bool.ml
+1 -1 metaprl/theories/czf/czf_itt_coset.ml
+1 -1 metaprl/theories/czf/czf_itt_coset.mli
+1 -1 metaprl/theories/czf/czf_itt_cyclic_group.ml
+1 -1 metaprl/theories/czf/czf_itt_cyclic_group.mli
+1 -1 metaprl/theories/czf/czf_itt_cyclic_subgroup.ml
+1 -1 metaprl/theories/czf/czf_itt_cyclic_subgroup.mli
+1 -1 metaprl/theories/czf/czf_itt_dall.ml
+1 -1 metaprl/theories/czf/czf_itt_dexists.ml
+1 -1 metaprl/theories/czf/czf_itt_empty.ml
+5 -4 metaprl/theories/czf/czf_itt_eq.mli
+1 -1 metaprl/theories/czf/czf_itt_equiv.ml
+6 -5 metaprl/theories/czf/czf_itt_equiv.mli
+1 -1 metaprl/theories/czf/czf_itt_exists.ml
+1 -1 metaprl/theories/czf/czf_itt_false.ml
+1 -1 metaprl/theories/czf/czf_itt_group.ml
+1 -1 metaprl/theories/czf/czf_itt_group.mli
+1 -1 metaprl/theories/czf/czf_itt_group_bvd.ml
+1 -1 metaprl/theories/czf/czf_itt_group_bvd.mli
+1 -1 metaprl/theories/czf/czf_itt_group_power.ml
+1 -1 metaprl/theories/czf/czf_itt_group_power.mli
+1 -1 metaprl/theories/czf/czf_itt_hom.ml
+1 -1 metaprl/theories/czf/czf_itt_hom.mli
+1 -1 metaprl/theories/czf/czf_itt_implies.ml
+1 -1 metaprl/theories/czf/czf_itt_inv_image.ml
+1 -1 metaprl/theories/czf/czf_itt_inv_image.mli
+1 -1 metaprl/theories/czf/czf_itt_isect.ml
+1 -1 metaprl/theories/czf/czf_itt_iso.ml
+1 -1 metaprl/theories/czf/czf_itt_iso.mli
+1 -1 metaprl/theories/czf/czf_itt_ker.ml
+1 -1 metaprl/theories/czf/czf_itt_ker.mli
+1 -1 metaprl/theories/czf/czf_itt_kleingroup.ml
+1 -1 metaprl/theories/czf/czf_itt_kleingroup.mli
+1 -1 metaprl/theories/czf/czf_itt_normal_subgroup.ml
+1 -1 metaprl/theories/czf/czf_itt_normal_subgroup.mli
+1 -1 metaprl/theories/czf/czf_itt_or.ml
+2 -1 metaprl/theories/czf/czf_itt_rel.mli
+1 -1 metaprl/theories/czf/czf_itt_sall.ml
+1 -1 metaprl/theories/czf/czf_itt_sep.ml
+1 -1 metaprl/theories/czf/czf_itt_set.ml
+3 -2 metaprl/theories/czf/czf_itt_set.mli
+1 -1 metaprl/theories/czf/czf_itt_set_bvd.ml
+1 -1 metaprl/theories/czf/czf_itt_set_bvd.mli
+2170 -2133 metaprl/theories/czf/czf_itt_set_bvd.prla
+1 -1 metaprl/theories/czf/czf_itt_set_ind.ml
+1 -1 metaprl/theories/czf/czf_itt_setdiff.ml
+1 -1 metaprl/theories/czf/czf_itt_sexists.ml
+1 -1 metaprl/theories/czf/czf_itt_singleton.ml
+1 -1 metaprl/theories/czf/czf_itt_subgroup.ml
+1 -1 metaprl/theories/czf/czf_itt_true.ml
+1 -1 metaprl/theories/czf/czf_itt_union.ml
+1 -1 metaprl/theories/experimental/compile/m_closure.ml
+1 -1 metaprl/theories/experimental/compile/m_cps.ml
+3 -2 metaprl/theories/experimental/compile/m_ir.mli
+1 -1 metaprl/theories/experimental/compile/m_post_parsing.ml
+1 -1 metaprl/theories/experimental/compile/m_prog.ml
+1 -1 metaprl/theories/experimental/compile/m_standardize.ml
+1 -1 metaprl/theories/experimental/compile/m_util.ml
+1 -1 metaprl/theories/experimental/compile/m_x86_regalloc.ml
+1 -1 metaprl/theories/experimental/compile/m_x86_spill.ml
+3 -3 metaprl/theories/experimental/compile/m_x86_term.ml
+34 -34 metaprl/theories/experimental/mcc/fir/type/m_fir_term.ml
+2 -2 metaprl/theories/experimental/mcc/fir/type/m_int.ml
+2 -2 metaprl/theories/experimental/mcc/fir/type/m_rawfloat.ml
+2 -2 metaprl/theories/experimental/mcc/fir/type/m_rawfloat.mli
+4 -4 metaprl/theories/experimental/mcc/fir/type/m_rawint.ml
+2 -2 metaprl/theories/experimental/mcc/fir/type/m_rawint.mli
+1 -1 metaprl/theories/fir/mfir_connect_base.ml
+4 -4 metaprl/theories/fir/mfir_connect_base.mli
+1 -1 metaprl/theories/fir/mfir_connect_exp.ml
+1 -1 metaprl/theories/fir/mfir_connect_ty.ml
+181 -180 metaprl/theories/fir/mfir_termOp.mli
+35 -34 metaprl/theories/fir/mfir_termOp_base.mli
+1 -1 metaprl/theories/itt/ctt_markov.ml
+1 -1 metaprl/theories/itt/itt_algebra_df.ml
+1 -1 metaprl/theories/itt/itt_atom.ml
+1 -1 metaprl/theories/itt/itt_bintree.ml
+1 -1 metaprl/theories/itt/itt_bintree.mli
+1 -1 metaprl/theories/itt/itt_bisect.ml
+1 -1 metaprl/theories/itt/itt_bunion.ml
+1 -1 metaprl/theories/itt/itt_collection.ml
+1 -1 metaprl/theories/itt/itt_collection.mli
+1 -1 metaprl/theories/itt/itt_cyclic_group.ml
+1 -1 metaprl/theories/itt/itt_cyclic_group.mli
+1 -1 metaprl/theories/itt/itt_datatree.ml
+1 -1 metaprl/theories/itt/itt_decidable.ml
+1 -1 metaprl/theories/itt/itt_dfun.ml
+1 -1 metaprl/theories/itt/itt_disect.ml
+3 -2 metaprl/theories/itt/itt_disect.mli
+18 -48 metaprl/theories/itt/itt_dprod.ml
+5 -4 metaprl/theories/itt/itt_dprod.mli
+1 -1 metaprl/theories/itt/itt_dprod_imp.ml
+6 -27 metaprl/theories/itt/itt_equal.ml
+2 -1 metaprl/theories/itt/itt_equal.mli
+1 -1 metaprl/theories/itt/itt_ext_equal.ml
+1 -1 metaprl/theories/itt/itt_fset.ml
+1 -1 metaprl/theories/itt/itt_fun.ml
+1 -1 metaprl/theories/itt/itt_group.ml
+1 -1 metaprl/theories/itt/itt_group.mli
+1 -1 metaprl/theories/itt/itt_grouplikeobj.ml
+1 -1 metaprl/theories/itt/itt_grouplikeobj.mli
+4 -23 metaprl/theories/itt/itt_int_arith.ml
+8 -9 metaprl/theories/itt/itt_int_base.ml
+10 -8 metaprl/theories/itt/itt_int_base.mli
+1 -1 metaprl/theories/itt/itt_int_ext.ml
+21 -1 metaprl/theories/itt/itt_int_ext.mli
+1 -1 metaprl/theories/itt/itt_inv_typing.ml
+1 -1 metaprl/theories/itt/itt_inv_typing.mli
+16 -35 metaprl/theories/itt/itt_isect.ml
+5 -2 metaprl/theories/itt/itt_isect.mli
+19 -37 metaprl/theories/itt/itt_list.ml
+3 -2 metaprl/theories/itt/itt_list.mli
+34 -53 metaprl/theories/itt/itt_list2.ml
+36 -70 metaprl/theories/itt/itt_logic.ml
+5 -4 metaprl/theories/itt/itt_logic.mli
+4 -5 metaprl/theories/itt/itt_nat.ml
+1 -1 metaprl/theories/itt/itt_pointwise.ml
+1 -1 metaprl/theories/itt/itt_pointwise2.ml
+14 -32 metaprl/theories/itt/itt_prec.ml
+9 -8 metaprl/theories/itt/itt_prec.mli
+1 -1 metaprl/theories/itt/itt_prod.ml
+1 -1 metaprl/theories/itt/itt_prop_decide.ml
+1 -1 metaprl/theories/itt/itt_quotient.ml
+3 -2 metaprl/theories/itt/itt_quotient.mli
+1 -1 metaprl/theories/itt/itt_quotient_group.ml
+1 -1 metaprl/theories/itt/itt_quotient_group.mli
+1 -1 metaprl/theories/itt/itt_rbtree.ml
+1 -1 metaprl/theories/itt/itt_record.ml
+1 -1 metaprl/theories/itt/itt_record0.ml
+1 -1 metaprl/theories/itt/itt_record_exm.ml
+1 -1 metaprl/theories/itt/itt_record_label.ml
+20 -43 metaprl/theories/itt/itt_rfun.ml
+11 -10 metaprl/theories/itt/itt_rfun.mli
+1 -1 metaprl/theories/itt/itt_set.ml
+3 -2 metaprl/theories/itt/itt_set.mli
+1 -1 metaprl/theories/itt/itt_singleton.ml
+1 -1 metaprl/theories/itt/itt_sortedtree.ml
+1 -1 metaprl/theories/itt/itt_squash.ml
+1 -1 metaprl/theories/itt/itt_squiggle.ml
+16 -32 metaprl/theories/itt/itt_srec.ml
+5 -4 metaprl/theories/itt/itt_srec.mli
+1 -1 metaprl/theories/itt/itt_struct.ml
+16 -41 metaprl/theories/itt/itt_struct2.ml
+1 -1 metaprl/theories/itt/itt_struct3.ml
+4 -1 metaprl/theories/itt/itt_struct3.mli
+1 -1 metaprl/theories/itt/itt_subset.ml
+1 -1 metaprl/theories/itt/itt_subset2.ml
+1 -1 metaprl/theories/itt/itt_subtype.ml
+1 -1 metaprl/theories/itt/itt_test.ml
+1 -1 metaprl/theories/itt/itt_tsquash.ml
+19 -39 metaprl/theories/itt/itt_union.ml
+3 -2 metaprl/theories/itt/itt_union.mli
+1 -1 metaprl/theories/itt/itt_unit.ml
+1 -1 metaprl/theories/itt/itt_void.ml
+13 -31 metaprl/theories/itt/itt_w.ml
+5 -4 metaprl/theories/itt/itt_w.mli
+1 -1 metaprl/theories/lf/main.ml
+1 -1 metaprl/theories/ocaml_sos/ocaml_expr_sos.ml
+1 -1 metaprl/theories/ocaml_sos/ocaml_logic.ml
+1 -1 metaprl/theories/ocaml_sos/ocaml_me_sos.ml
+1 -1 metaprl/theories/ocaml_sos/ocaml_mt_sos.ml
+1 -1 metaprl/theories/ocaml_sos/ocaml_patt_sos.ml
+1 -1 metaprl/theories/ocaml_sos/ocaml_sig_sos.ml
+1 -1 metaprl/theories/ocaml_sos/ocaml_str_sos.ml
+1 -1 metaprl/theories/ocaml_sos/ocaml_type_sos.ml
+0 -2 metaprl/theories/phobos/phobos_base.ml
+0 -2 metaprl/theories/phobos/phobos_base.mli
+0 -2 metaprl/theories/phobos/phobos_theory.ml
+1 -1 metaprl/theories/tptp/tptp.ml
+7 -6 metaprl/theories/tptp/tptp.mli
+10 -4 metaprl/theories/tptp/tptp_cache.ml
+1 -1 metaprl/theories/tptp/tptp_cache.mli
+1 -1 metaprl/theories/tptp/tptp_lex.mll
+19 -10 metaprl/theories/tptp/tptp_load.ml
+45 -20 metaprl/theories/tptp/tptp_prove.ml
+1 -1 metaprl/util/ocamldep.mll
+2 -2 mpcompiler/mmc/core/core_test.ml
+1 -1 mpcompiler/mmc/core/mmc_core_util.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-11 15:34:52 -0700 (Fri, 11 Jul 2003)
Revision: 4731
Log message:

      Added a little more code for type inference.  The current
      code does not handle bounded quantifiers correctly.
      

Changes  Path
+64 -13 mpcompiler/mmc/core/mmc_core_type_infer.ml

Changes by: ( at unknown.email)
Date: 2003-07-13 03:34:55 -0700 (Sun, 13 Jul 2003)
Revision: 4736
Log message:

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

Changes  Path
Copied metaprl-branches/bound_contexts
Copied mpcompiler-branches/bound_contexts
Copied texinputs-branches/bound_contexts
Deleted texinputs-branches/bound_contexts/1cm.sty
Deleted texinputs-branches/bound_contexts/1cml.sty
Deleted texinputs-branches/bound_contexts/Makefile
Deleted texinputs-branches/bound_contexts/Makefile-common
Deleted texinputs-branches/bound_contexts/PPR-macros.tex
Deleted texinputs-branches/bound_contexts/PPRmyppr.sty
Deleted texinputs-branches/bound_contexts/bcp.bib
Deleted texinputs-branches/bound_contexts/citlogo.eps
Deleted texinputs-branches/bound_contexts/citlogo2.eps
Deleted texinputs-branches/bound_contexts/config.ppr
Deleted texinputs-branches/bound_contexts/cornell-logo.eps
Deleted texinputs-branches/bound_contexts/dag50.eps
Deleted texinputs-branches/bound_contexts/der.tex
Deleted texinputs-branches/bound_contexts/gate.eps
Deleted texinputs-branches/bound_contexts/gate.pdf
Deleted texinputs-branches/bound_contexts/include.tex
Deleted texinputs-branches/bound_contexts/llncs.cls
Deleted texinputs-branches/bound_contexts/omscmsy.fd
Deleted texinputs-branches/bound_contexts/ot1cmr.fd
Deleted texinputs-branches/bound_contexts/ot1cmss.fd
Deleted texinputs-branches/bound_contexts/ot1lcmss.fd
Deleted texinputs-branches/bound_contexts/ot1lcmtt.fd
Deleted texinputs-branches/bound_contexts/pprpdf
Deleted texinputs-branches/bound_contexts/proof.sty
Deleted texinputs-branches/bound_contexts/slides-nogin.cls
Deleted texinputs-branches/bound_contexts/splncs.bst
Deleted texinputs-branches/bound_contexts/umsa.fd
Deleted texinputs-branches/bound_contexts/umsb.fd

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-13 18:39:54 -0700 (Sun, 13 Jul 2003)
Revision: 4738
Log message:

      Core_type_infer now compiles, though completely untested.
      Fixed a dumb dependency bug in OMakefile.
      

Changes  Path
+3 -1 metaprl/OMakefile
+1 -1 metaprl/filter/boot/proof_term_boot.ml
+7 -5 metaprl/mllib/weak_memo.ml
+0 -5 metaprl/support/tactics/simp_typeinf.ml
+0 -2 metaprl/support/tactics/simp_typeinf.mli
+7 -0 metaprl/support/tactics/var.ml
+3 -0 metaprl/support/tactics/var.mli
+3 -16 metaprl/theories/base/base_theory.mlz
Added mpcompiler/mmc/core/Files
Properties mpcompiler/mmc/core/Files
+2 -8 mpcompiler/mmc/core/Makefile
+2 -8 mpcompiler/mmc/core/OMakefile
+82 -45 mpcompiler/mmc/core/mmc_core_type_infer.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-14 11:00:00 -0700 (Mon, 14 Jul 2003)
Revision: 4739
Log message:

      Some minor changes.
      
      Did not change Term_match_table.  We'll have to decide if we
      want default cases.
      
      Core_type_erase also has an issue with default cases.
      Specifically, all types are erased, but all variables
      are left wrapped, like erase{'v}.  I'm not sure we want
      to add a default case.
      

Changes  Path
+9 -9 metaprl/refiner/reflib/term_match_table.ml
+3 -7 metaprl/support/tactics/simp_typeinf.ml
+1 -0 mpcompiler/mmc/core/Files
+4 -9 mpcompiler/mmc/core/core_test.ml
+2 -1 mpcompiler/mmc/core/core_test.mli
Added mpcompiler/mmc/core/mmc_core_theory.ml
Properties mpcompiler/mmc/core/mmc_core_theory.ml
Added mpcompiler/mmc/core/mmc_core_theory.mli
Properties mpcompiler/mmc/core/mmc_core_theory.mli
+7 -12 mpcompiler/mmc/core/mmc_core_type_erase.ml
+2 -2 mpcompiler/mmc/core/mmc_core_type_erase.mli
+10 -5 mpcompiler/mmc/core/mmc_core_type_infer.ml

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-14 11:00:22 -0700 (Mon, 14 Jul 2003)
Revision: 4740
Log message:

      Forgot to add this file.
      

Changes  Path
Added mpcompiler/mmc/core/mmc_core_type_infer.mli
Properties mpcompiler/mmc/core/mmc_core_type_infer.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-15 17:07:35 -0700 (Tue, 15 Jul 2003)
Revision: 4749
Log message:

      Merged CPS conversion and sequent representation of
      quantifiers onto the trunk.
      

Changes  Path
+3 -0 mpcompiler/mmc/core/Files
Added mpcompiler/mmc/core/core_sequent.ml
Properties mpcompiler/mmc/core/core_sequent.ml
Added mpcompiler/mmc/core/core_sequent.mli
Properties mpcompiler/mmc/core/core_sequent.mli
+1 -1 mpcompiler/mmc/core/core_test.ml
+58 -16 mpcompiler/mmc/core/mmc_core_cps.ml
Added mpcompiler/mmc/core/mmc_core_cps.mli
Properties mpcompiler/mmc/core/mmc_core_cps.mli
+4 -1 mpcompiler/mmc/core/mmc_core_tast.ml
+1 -0 mpcompiler/mmc/core/mmc_core_tast.mli
+1 -0 mpcompiler/mmc/core/mmc_core_theory.ml
+10 -0 mpcompiler/mmc/core/mmc_core_type_erase.ml
+1 -1 mpcompiler/mmc/core/mmc_core_type_infer.ml
Added mpcompiler/mmc/core/mmc_core_type_util.ml
Properties mpcompiler/mmc/core/mmc_core_type_util.ml
Added mpcompiler/mmc/core/mmc_core_type_util.mli
Properties mpcompiler/mmc/core/mmc_core_type_util.mli

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2003-07-18 19:29:12 -0700 (Fri, 18 Jul 2003)
Revision: 4761
Log message:

      Added sequents to <:con< ... >> quotation.
      Here's a short summary of syntax:
      
         e ::= sequent [args] { hyps >- con_term list }
         args ::= con_term list  -- The usual syntax for these terms
         hyp ::= <H> | <H[con_terms]>
             |   <$e$>           -- $e$ should be a list of hypothesis terms
             |   v:con_term
             |   $v$:con_term
      
      This is the first pass, undoubtly we'll need some tuning.
      

Changes  Path
+6 -0 metaprl/filter/base/filter_type.ml
+30 -1 metaprl/filter/filter/filter_parse.ml
+62 -6 metaprl/filter/filter/term_grammar.ml
+1 -1 metaprl/refiner/refsig/term_sig.ml
+1 -3 mpcompiler/mmc/core/mmc_core_type_infer.ml

Changes by: ( at unknown.email)
Date: 2003-07-23 14:40:47 -0700 (Wed, 23 Jul 2003)
Revision: 4768
Log message:

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

Changes  Path
Copied mpcompiler-branches/mojave_sequents

Changes by: Cristian Tapus (crt at cs.caltech.edu)
Date: 2003-07-23 14:40:47 -0700 (Wed, 23 Jul 2003)
Revision: 4769
Log message:

      Added sequents code to all the files...
      

Changes  Path
+2 -5 mpcompiler-branches/mojave_sequents/mmc/core/core_sequent.ml
+8 -2 mpcompiler-branches/mojave_sequents/mmc/core/core_test.ml
+14 -3 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast.ml
+6 -1 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_ast.mli
+6 -6 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_cps.ml
+2 -2 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_name.ml
+10 -8 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_tast.ml
+3 -4 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_tast.mli
+125 -30 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_type_check.ml
+23 -6 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_type_erase.ml
+67 -30 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_type_infer.ml
+38 -1 mpcompiler-branches/mojave_sequents/mmc/core/mmc_core_type_util.ml

Changes by: ( at unknown.email)
Date: 2003-07-28 17:33:02 -0700 (Mon, 28 Jul 2003)
Revision: 4782
Log message:

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

Changes  Path
Copied metaprl-branches/bound_contexts2
Copied mpcompiler-branches/bound_contexts2
Copied texinputs-branches/bound_contexts2
Deleted texinputs-branches/bound_contexts2/1cm.sty
Deleted texinputs-branches/bound_contexts2/1cml.sty
Deleted texinputs-branches/bound_contexts2/Makefile
Deleted texinputs-branches/bound_contexts2/Makefile-common
Deleted texinputs-branches/bound_contexts2/PPR-macros.tex
Deleted texinputs-branches/bound_contexts2/PPRmyppr.sty
Deleted texinputs-branches/bound_contexts2/bcp.bib
Deleted texinputs-branches/bound_contexts2/citlogo.eps
Deleted texinputs-branches/bound_contexts2/citlogo2.eps
Deleted texinputs-branches/bound_contexts2/config.ppr
Deleted texinputs-branches/bound_contexts2/cornell-logo.eps
Deleted texinputs-branches/bound_contexts2/dag50.eps
Deleted texinputs-branches/bound_contexts2/der.tex
Deleted texinputs-branches/bound_contexts2/gate.eps
Deleted texinputs-branches/bound_contexts2/gate.pdf
Deleted texinputs-branches/bound_contexts2/include.tex
Deleted texinputs-branches/bound_contexts2/omscmsy.fd
Deleted texinputs-branches/bound_contexts2/ot1cmr.fd
Deleted texinputs-branches/bound_contexts2/ot1cmss.fd
Deleted texinputs-branches/bound_contexts2/ot1lcmss.fd
Deleted texinputs-branches/bound_contexts2/ot1lcmtt.fd
Deleted texinputs-branches/bound_contexts2/pprpdf
Deleted texinputs-branches/bound_contexts2/proof.sty
Deleted texinputs-branches/bound_contexts2/slides-nogin.cls
Deleted texinputs-branches/bound_contexts2/splncs.bst
Deleted texinputs-branches/bound_contexts2/umsa.fd
Deleted texinputs-branches/bound_contexts2/umsb.fd