Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1997-08-06 09:18:55 -0700 (Wed, 06 Aug 1997)
Revision: 2047
Log message:

      This is an ocaml version with subtyping, type inference,
      d and eqcd tactics.  It is a basic system, but not debugged.
      

Changes	Path
+4 -1	metaprl/README
Added	metaprl/clib/Makefile
Properties	metaprl/clib/Makefile
Added	metaprl/clib/punix.ml
Properties	metaprl/clib/punix.ml
Added	metaprl/clib/punix.mli
Properties	metaprl/clib/punix.mli
Added	metaprl/clib/putenv.c
Properties	metaprl/clib/putenv.c
+16 -10	metaprl/editor/emacs/caml.el
Added	metaprl/editor/ml/display_package.ml
Properties	metaprl/editor/ml/display_package.ml
Added	metaprl/editor/ml/display_package.mli
Properties	metaprl/editor/ml/display_package.mli
Added	metaprl/editor/ml/display_package_graph.ml
Properties	metaprl/editor/ml/display_package_graph.ml
Added	metaprl/editor/ml/display_package_graph.mli
Properties	metaprl/editor/ml/display_package_graph.mli
Added	metaprl/editor/ml/display_theory_item.ml
Properties	metaprl/editor/ml/display_theory_item.ml
Added	metaprl/editor/ml/display_theory_item.mli
Properties	metaprl/editor/ml/display_theory_item.mli
Added	metaprl/editor/ml/edit_type.ml
Properties	metaprl/editor/ml/edit_type.ml
Added	metaprl/editor/ml/edit_type.mli
Properties	metaprl/editor/ml/edit_type.mli
Added	metaprl/editor/ml/editor_init.ml
Properties	metaprl/editor/ml/editor_init.ml
Added	metaprl/editor/ml/editor_init.mli
Properties	metaprl/editor/ml/editor_init.mli
Added	metaprl/editor/ml/file_util.ml
Properties	metaprl/editor/ml/file_util.ml
Added	metaprl/editor/ml/file_util.mli
Properties	metaprl/editor/ml/file_util.mli
Added	metaprl/editor/ml/imp_dag.ml
Properties	metaprl/editor/ml/imp_dag.ml
Added	metaprl/editor/ml/imp_dag.mli
Properties	metaprl/editor/ml/imp_dag.mli
Added	metaprl/editor/ml/main.ml
Properties	metaprl/editor/ml/main.ml
Added	metaprl/editor/ml/main.mli
Properties	metaprl/editor/ml/main.mli
Added	metaprl/editor/ml/package_graph.ml
Properties	metaprl/editor/ml/package_graph.ml
Added	metaprl/editor/ml/package_graph.mli
Properties	metaprl/editor/ml/package_graph.mli
Added	metaprl/editor/ml/package_info.ml
Properties	metaprl/editor/ml/package_info.ml
Added	metaprl/editor/ml/package_info.mli
Properties	metaprl/editor/ml/package_info.mli
Added	metaprl/editor/ml/package_int.ml
Properties	metaprl/editor/ml/package_int.ml
Added	metaprl/editor/ml/package_int.mli
Properties	metaprl/editor/ml/package_int.mli
Added	metaprl/editor/ml/package_io.ml
Properties	metaprl/editor/ml/package_io.ml
Added	metaprl/editor/ml/package_io.mli
Properties	metaprl/editor/ml/package_io.mli
Added	metaprl/editor/ml/package_util.ml
Properties	metaprl/editor/ml/package_util.ml
Added	metaprl/editor/ml/package_util.mli
Properties	metaprl/editor/ml/package_util.mli
Added	metaprl/editor/ml/proof.ml
Properties	metaprl/editor/ml/proof.ml
Added	metaprl/editor/ml/proof.mli
Properties	metaprl/editor/ml/proof.mli
Added	metaprl/editor/ml/proof_edit.ml
Properties	metaprl/editor/ml/proof_edit.ml
Added	metaprl/editor/ml/proof_edit.mli
Properties	metaprl/editor/ml/proof_edit.mli
Added	metaprl/editor/ml/proof_step.ml
Properties	metaprl/editor/ml/proof_step.ml
Added	metaprl/editor/ml/proof_step.mli
Properties	metaprl/editor/ml/proof_step.mli
Added	metaprl/editor/ml/shell.ml
Properties	metaprl/editor/ml/shell.ml
Added	metaprl/editor/ml/shell.mli
Properties	metaprl/editor/ml/shell.mli
+19 -5	metaprl/filter/Makefile
+10 -6	metaprl/filter/filter_ast.mli
+425 -374	metaprl/filter/filter_cache.ml
+9 -49	metaprl/filter/filter_cache.mli
+7 -3	metaprl/filter/filter_hash.ml
+11 -7	metaprl/filter/filter_hash.mli
+141 -113	metaprl/filter/filter_parse.ml
+8 -5	metaprl/filter/filter_process_type.mlz
+151 -110	metaprl/filter/filter_summary.ml
+59 -43	metaprl/filter/filter_summary.mli
Added	metaprl/filter/filter_summary_base.ml
Properties	metaprl/filter/filter_summary_base.ml
+139 -131	metaprl/filter/filter_summary_io.ml
+16 -16	metaprl/filter/filter_summary_io.mli
Added	metaprl/filter/filter_summary_type.mlz
Properties	metaprl/filter/filter_summary_type.mlz
+89 -33	metaprl/filter/filter_summary_util.ml
+36 -5	metaprl/filter/filter_summary_util.mli
+4 -4	metaprl/filter/filter_type.mlz
+7 -3	metaprl/filter/free_vars.mli
Added	metaprl/filter/infix.ml
Properties	metaprl/filter/infix.ml
+5 -1	metaprl/filter/infix.mli
+42 -14	metaprl/filter/prlcomp.ml
+12 -7	metaprl/filter/term_grammar.ml
+5 -1	metaprl/filter/term_grammar.mli
Added	metaprl/horus/Makefile
Properties	metaprl/horus/Makefile
Added	metaprl/horus/opname.ml
Properties	metaprl/horus/opname.ml
Added	metaprl/horus/opname.mli
Properties	metaprl/horus/opname.mli
Added	metaprl/horus/term.ml
Properties	metaprl/horus/term.ml
Added	metaprl/horus/term.mli
Properties	metaprl/horus/term.mli
Added	metaprl/horus/util.ml
Properties	metaprl/horus/util.ml
Added	metaprl/horus/util.mli
Properties	metaprl/horus/util.mli
+35 -8	metaprl/mk/config
Added	metaprl/mk/preface
Properties	metaprl/mk/preface
Added	metaprl/mllib/Makefile
Properties	metaprl/mllib/Makefile
Added	metaprl/mllib/array_util.ml
Properties	metaprl/mllib/array_util.ml
Added	metaprl/mllib/array_util.mli
Properties	metaprl/mllib/array_util.mli
Added	metaprl/mllib/ctype.ml
Properties	metaprl/mllib/ctype.ml
Added	metaprl/mllib/ctype.mli
Properties	metaprl/mllib/ctype.mli
Added	metaprl/mllib/debug.ml
Properties	metaprl/mllib/debug.ml
Added	metaprl/mllib/debug.mli
Properties	metaprl/mllib/debug.mli
Added	metaprl/mllib/env_arg.ml
Properties	metaprl/mllib/env_arg.ml
Added	metaprl/mllib/env_arg.mli
Properties	metaprl/mllib/env_arg.mli
Added	metaprl/mllib/file_base.ml
Properties	metaprl/mllib/file_base.ml
Added	metaprl/mllib/file_base.mli
Properties	metaprl/mllib/file_base.mli
Added	metaprl/mllib/file_base_type.mli
Properties	metaprl/mllib/file_base_type.mli
Added	metaprl/mllib/file_type_base.ml
Properties	metaprl/mllib/file_type_base.ml
Added	metaprl/mllib/file_type_base.mli
Properties	metaprl/mllib/file_type_base.mli
Added	metaprl/mllib/file_util.ml
Properties	metaprl/mllib/file_util.ml
Added	metaprl/mllib/file_util.mli
Properties	metaprl/mllib/file_util.mli
Added	metaprl/mllib/list_util.ml
Properties	metaprl/mllib/list_util.ml
Added	metaprl/mllib/list_util.mli
Properties	metaprl/mllib/list_util.mli
Added	metaprl/mllib/ref_util.ml
Properties	metaprl/mllib/ref_util.ml
Added	metaprl/mllib/ref_util.mli
Properties	metaprl/mllib/ref_util.mli
Added	metaprl/mllib/string_util.ml
Properties	metaprl/mllib/string_util.ml
Added	metaprl/mllib/string_util.mli
Properties	metaprl/mllib/string_util.mli
+1 -9	metaprl/refiner/Makefile
Deleted	metaprl/refiner/array_util.ml
Deleted	metaprl/refiner/array_util.mli
Deleted	metaprl/refiner/ctype.ml
Deleted	metaprl/refiner/ctype.mli
Deleted	metaprl/refiner/debug.ml
Deleted	metaprl/refiner/debug.mli
Deleted	metaprl/refiner/env_arg.ml
Deleted	metaprl/refiner/env_arg.mli
Deleted	metaprl/refiner/file_util.ml
Deleted	metaprl/refiner/file_util.mli
Deleted	metaprl/refiner/list_util.ml
Deleted	metaprl/refiner/list_util.mli
Deleted	metaprl/refiner/ref_util.ml
Deleted	metaprl/refiner/ref_util.mli
+19 -0	metaprl/refiner/refine.ml
+26 -22	metaprl/refiner/rformat.mli
Deleted	metaprl/refiner/string_util.ml
Deleted	metaprl/refiner/string_util.mli
+46 -0	metaprl/refiner/term.ml
+26 -0	metaprl/refiner/term.mli
+13 -6	metaprl/refiner/term_util.ml
+1 -0	metaprl/theories/.cprc
+3 -2	metaprl/theories/base/Makefile
+6 -1	metaprl/theories/base/base_theory.mlz
Added	metaprl/theories/base/typeinf.ml
Properties	metaprl/theories/base/typeinf.ml
Added	metaprl/theories/base/typeinf.mli
Properties	metaprl/theories/base/typeinf.mli
+7 -4	metaprl/theories/itt/Makefile
+32 -8	metaprl/theories/itt/itt_atom.ml
+16 -2	metaprl/theories/itt/itt_atom.mli
+121 -28	metaprl/theories/itt/itt_dfun.ml
+48 -4	metaprl/theories/itt/itt_dfun.mli
+130 -11	metaprl/theories/itt/itt_dprod.ml
+40 -0	metaprl/theories/itt/itt_dprod.mli
+88 -104	metaprl/theories/itt/itt_equal.ml
+31 -3	metaprl/theories/itt/itt_equal.mli
Added	metaprl/theories/itt/itt_ext_equal.ml
Properties	metaprl/theories/itt/itt_ext_equal.ml
Added	metaprl/theories/itt/itt_ext_equal.mli
Properties	metaprl/theories/itt/itt_ext_equal.mli
+58 -8	metaprl/theories/itt/itt_fun.ml
+21 -0	metaprl/theories/itt/itt_fun.mli
+52 -12	metaprl/theories/itt/itt_int.ml
+19 -0	metaprl/theories/itt/itt_int.mli
+61 -12	metaprl/theories/itt/itt_isect.ml
+25 -0	metaprl/theories/itt/itt_isect.mli
+125 -11	metaprl/theories/itt/itt_list.ml
+42 -0	metaprl/theories/itt/itt_list.mli
+105 -8	metaprl/theories/itt/itt_logic.ml
+33 -0	metaprl/theories/itt/itt_logic.mli
+43 -0	metaprl/theories/itt/itt_prec.ml
+16 -0	metaprl/theories/itt/itt_prec.mli
+54 -7	metaprl/theories/itt/itt_prod.ml
+21 -0	metaprl/theories/itt/itt_prod.mli
+69 -7	metaprl/theories/itt/itt_quotient.ml
+29 -0	metaprl/theories/itt/itt_quotient.mli
+109 -10	metaprl/theories/itt/itt_rfun.ml
+39 -0	metaprl/theories/itt/itt_rfun.mli
+156 -2	metaprl/theories/itt/itt_set.ml
+45 -1	metaprl/theories/itt/itt_set.mli
Added	metaprl/theories/itt/itt_squash.ml
Properties	metaprl/theories/itt/itt_squash.ml
Added	metaprl/theories/itt/itt_squash.mli
Properties	metaprl/theories/itt/itt_squash.mli
+39 -0	metaprl/theories/itt/itt_srec.ml
+14 -0	metaprl/theories/itt/itt_srec.mli
+167 -0	metaprl/theories/itt/itt_struct.ml
+45 -0	metaprl/theories/itt/itt_struct.mli
+144 -17	metaprl/theories/itt/itt_subtype.ml
+51 -7	metaprl/theories/itt/itt_subtype.mli
+134 -9	metaprl/theories/itt/itt_union.ml
+41 -0	metaprl/theories/itt/itt_union.mli
Added	metaprl/theories/itt/itt_unit.ml
Properties	metaprl/theories/itt/itt_unit.ml
Added	metaprl/theories/itt/itt_unit.mli
Properties	metaprl/theories/itt/itt_unit.mli
+46 -4	metaprl/theories/itt/itt_void.ml
+24 -0	metaprl/theories/itt/itt_void.mli
Added	metaprl/theories/itt/main.ml
Properties	metaprl/theories/itt/main.ml
Added	metaprl/theories/itt/main.mli
Properties	metaprl/theories/itt/main.mli
Added	metaprl/theories/itt/test.mli
Properties	metaprl/theories/itt/test.mli
Added	metaprl/theories/rewrite/Makefile
Properties	metaprl/theories/rewrite/Makefile
Added	metaprl/theories/rewrite/rw_beta.ml
Properties	metaprl/theories/rewrite/rw_beta.ml
Added	metaprl/theories/rewrite/rw_beta.mli
Properties	metaprl/theories/rewrite/rw_beta.mli
+1 -1	metaprl/theories/tactic/Makefile
+12 -0	metaprl/theories/tactic/tacticals.ml
+6 -0	metaprl/theories/tactic/tacticals.mli