Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-07-21 15:47:13 -0700 (Tue, 21 Jul 1998)
Revision: 2336
Log message:

      Added NL toploop so that we can compile NL native code.
      

Changes	Path
+1 -1	metaprl/Makefile
Properties	metaprl/editor/ml
+71 -12	metaprl/editor/ml/Makefile
+2 -1	metaprl/editor/ml/io_proof.ml
+1 -1	metaprl/editor/ml/nl
+57 -1	metaprl/editor/ml/nl.ml
+57 -0	metaprl/editor/ml/nl.mli
Added	metaprl/editor/ml/nl_top.ml
Properties	metaprl/editor/ml/nl_top.ml
Added	metaprl/editor/ml/nl_top.mli
Properties	metaprl/editor/ml/nl_top.mli
+1 -1	metaprl/editor/ml/package_df.ml
+99 -233	metaprl/editor/ml/package_info.ml
+0 -9	metaprl/editor/ml/package_info.mli
+1 -1	metaprl/editor/ml/package_int.ml
+1 -1	metaprl/editor/ml/package_type.mlz
+3 -3	metaprl/editor/ml/proof.ml
+1 -1	metaprl/editor/ml/proof.mli
+1 -1	metaprl/editor/ml/proof_edit.ml
+5 -58	metaprl/editor/ml/proof_step.ml
+1 -0	metaprl/editor/ml/proof_step.mli
+585 -575	metaprl/editor/ml/shell.ml
+64 -62	metaprl/editor/ml/shell.mli
Added	metaprl/editor/ml/shell_nl.ml
Properties	metaprl/editor/ml/shell_nl.ml
Added	metaprl/editor/ml/shell_nl.mli
Properties	metaprl/editor/ml/shell_nl.mli
+1 -1	metaprl/editor/ml/shell_null.ml
+392 -279	metaprl/editor/ml/shell_p4.ml
+7 -15	metaprl/editor/ml/shell_p4.mli
Added	metaprl/editor/ml/shell_p4_type.mlz
Properties	metaprl/editor/ml/shell_p4_type.mlz
+1 -1	metaprl/editor/ml/shell_rewrite.ml
+1 -1	metaprl/editor/ml/shell_rule.ml
+1 -1	metaprl/editor/ml/x.ml
+2 -2	metaprl/editor/ml/y.ml
Properties	metaprl/filter
+13 -22	metaprl/filter/Makefile
+1 -1	metaprl/filter/buffer.ml
+1 -1	metaprl/filter/filter_ast.ml
+24 -11	metaprl/filter/filter_bin.ml
+1 -1	metaprl/filter/filter_cache.ml
+3 -2	metaprl/filter/filter_cache_fun.ml
+1 -1	metaprl/filter/filter_comment.ml
+9 -2	metaprl/filter/filter_exn.ml
+1 -1	metaprl/filter/filter_grammar.ml
+1 -1	metaprl/filter/filter_hash.ml
+1 -1	metaprl/filter/filter_html.ml
+31 -2	metaprl/filter/filter_main.ml
+1 -1	metaprl/filter/filter_ocaml.ml
+42 -19	metaprl/filter/filter_parse.ml
+132 -13	metaprl/filter/filter_prog.ml
+1 -0	metaprl/filter/filter_prog.mli
+17 -2	metaprl/filter/filter_summary.ml
+1 -0	metaprl/filter/filter_summary.mli
+1 -1	metaprl/filter/filter_summary_io.ml
+1 -1	metaprl/filter/filter_summary_type.mlz
+1 -1	metaprl/filter/filter_summary_util.ml
+1 -1	metaprl/filter/filter_util.ml
+1 -1	metaprl/filter/free_vars.ml
+1 -1	metaprl/filter/mLast_util.ml
+2 -1	metaprl/filter/prlcomp.ml
+1 -1	metaprl/filter/term_grammar.ml
+1 -1	metaprl/filter/term_quote.ml
+1 -1	metaprl/library/ascii_scan.ml
+1 -1	metaprl/library/basic.ml
+1 -1	metaprl/library/bigInt.ml
+1 -1	metaprl/library/db.ml
+1 -1	metaprl/library/definition.ml
+1 -1	metaprl/library/int32.ml
+1 -1	metaprl/library/library.ml
+1 -1	metaprl/library/library_eval.ml
+2 -2	metaprl/library/library_type_base.ml
+1 -1	metaprl/library/link.ml
+1 -1	metaprl/library/mathBus.ml
+1 -1	metaprl/library/mbterm.ml
+1 -1	metaprl/library/nuprl5.ml
+1 -1	metaprl/library/object_id.ml
+1 -1	metaprl/library/oidtable.ml
+1 -1	metaprl/library/orb.ml
+1 -1	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
+37 -16	metaprl/mk/config
+1 -1	metaprl/mllib/Makefile
+1 -1	metaprl/mllib/array_util.ml
+1 -1	metaprl/mllib/bitset.ml
+1 -1	metaprl/mllib/ctype.ml
Deleted	metaprl/mllib/debug.ml
Deleted	metaprl/mllib/debug.mli
+1 -1	metaprl/mllib/debug_set.ml
+1 -1	metaprl/mllib/env_arg.ml
+1 -1	metaprl/mllib/file_base.ml
+1 -1	metaprl/mllib/file_type_base.ml
+1 -1	metaprl/mllib/file_util.ml
+1 -1	metaprl/mllib/filename_util.ml
+1 -1	metaprl/mllib/imp_dag.ml
+1 -1	metaprl/mllib/list_util.ml
+1 -1	metaprl/mllib/memo.ml
Added	metaprl/mllib/nl_debug.ml
Properties	metaprl/mllib/nl_debug.ml
Added	metaprl/mllib/nl_debug.mli
Properties	metaprl/mllib/nl_debug.mli
+1 -1	metaprl/mllib/precedence.ml
+1 -1	metaprl/mllib/ref_util.ml
+1 -1	metaprl/mllib/string_util.ml
+1 -1	metaprl/refiner/refbase/opname.ml
+1 -1	metaprl/refiner/refiner/refine.mlp
+1 -1	metaprl/refiner/refiner/rewrite.mlp
+1 -1	metaprl/refiner/reflib/dform.ml
+1 -1	metaprl/refiner/reflib/dform_print.ml
+1 -1	metaprl/refiner/reflib/ml_file.ml
+1 -1	metaprl/refiner/reflib/ml_format.ml
+1 -1	metaprl/refiner/reflib/ml_print.ml
+1 -1	metaprl/refiner/reflib/ml_string.ml
+1 -1	metaprl/refiner/reflib/refine_exn.ml
+2 -2	metaprl/refiner/reflib/resource.ml
+1 -1	metaprl/refiner/reflib/resource.mli
+1 -1	metaprl/refiner/reflib/rformat.ml
+1 -1	metaprl/refiner/reflib/simple_print.ml
+1 -1	metaprl/refiner/reflib/term_copy.ml
+1 -1	metaprl/refiner/reflib/term_dtable.ml
+1 -1	metaprl/refiner/reflib/term_stable.ml
+1 -1	metaprl/refiner/reflib/term_table.ml
+1 -1	metaprl/refiner/reflib/theory.ml
+1 -1	metaprl/refiner/term_ds/term_base_ds.mlp
+1 -1	metaprl/refiner/term_ds/term_ds.ml
+1 -1	metaprl/refiner/term_ds/term_subst_ds.mlp
+1 -1	metaprl/refiner/term_gen/term_addr_gen.mlp
+1 -1	metaprl/refiner/term_gen/term_man_gen.mlp
+1 -1	metaprl/refiner/term_std/term_base_std.mlp
+1 -1	metaprl/refiner/term_std/term_std.ml
+1 -1	metaprl/refiner/term_std/term_subst_std.mlp
+42 -21	metaprl/theories/base/base_auto_tactic.ml
+13 -4	metaprl/theories/base/base_auto_tactic.mli
+19 -1	metaprl/theories/base/base_cache.ml
+4 -0	metaprl/theories/base/base_cache.mli
+1 -1	metaprl/theories/base/base_dform.ml
+21 -2	metaprl/theories/base/base_dtactic.ml
+6 -2	metaprl/theories/base/base_dtactic.mli
+1 -1	metaprl/theories/base/evaluator.ml
+1 -1	metaprl/theories/base/nuprl_font.ml
+1 -1	metaprl/theories/base/summary.ml
+20 -2	metaprl/theories/base/typeinf.ml
+4 -0	metaprl/theories/base/typeinf.mli
+1 -1	metaprl/theories/czf/czf_itt_all.ml
+1 -1	metaprl/theories/czf/czf_itt_and.ml
+1 -2	metaprl/theories/czf/czf_itt_axioms.ml
Binary	metaprl/theories/czf/czf_itt_axioms.prlb
+1 -25	metaprl/theories/czf/czf_itt_dall.ml
+1 -26	metaprl/theories/czf/czf_itt_dexists.ml
+0 -9	metaprl/theories/czf/czf_itt_dexists.mli
+1 -1	metaprl/theories/czf/czf_itt_empty.ml
+1 -8	metaprl/theories/czf/czf_itt_eq.ml
+9 -6	metaprl/theories/czf/czf_itt_eq.mli
+2 -2	metaprl/theories/czf/czf_itt_eq_inner.ml
+2 -2	metaprl/theories/czf/czf_itt_eq_inner.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_implies.ml
+1 -1	metaprl/theories/czf/czf_itt_or.ml
+1 -1	metaprl/theories/czf/czf_itt_pre_set.ml
+2 -2	metaprl/theories/czf/czf_itt_rel.ml
+2 -2	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
+2 -1	metaprl/theories/czf/czf_itt_set.ml
+3 -3	metaprl/theories/czf/czf_itt_set.mli
+1 -1	metaprl/theories/czf/czf_itt_set_ext.ml
+1 -1	metaprl/theories/czf/czf_itt_set_ind.ml
+1 -1	metaprl/theories/czf/czf_itt_sexists.ml
+1 -1	metaprl/theories/czf/czf_itt_small.ml
+1 -1	metaprl/theories/czf/czf_itt_true.ml
+1 -1	metaprl/theories/czf/czf_itt_union.ml
+1 -1	metaprl/theories/itt/itt_arith.ml
+1 -1	metaprl/theories/itt/itt_atom.ml
+1 -0	metaprl/theories/itt/itt_derive.ml
+3 -3	metaprl/theories/itt/itt_derive.mli
+1 -1	metaprl/theories/itt/itt_dfun.ml
+1 -1	metaprl/theories/itt/itt_dprod.ml
+20 -2	metaprl/theories/itt/itt_equal.ml
+14 -10	metaprl/theories/itt/itt_equal.mli
+1 -1	metaprl/theories/itt/itt_ext_equal.ml
+1 -1	metaprl/theories/itt/itt_fun.ml
+1 -1	metaprl/theories/itt/itt_int.ml
+1 -1	metaprl/theories/itt/itt_isect.ml
+1 -1	metaprl/theories/itt/itt_list.ml
+2 -1	metaprl/theories/itt/itt_logic.ml
+17 -17	metaprl/theories/itt/itt_logic.mli
+1 -1	metaprl/theories/itt/itt_prec.ml
+1 -1	metaprl/theories/itt/itt_prod.ml
+1 -1	metaprl/theories/itt/itt_quotient.ml
+1 -1	metaprl/theories/itt/itt_redrules.ml
+1 -1	metaprl/theories/itt/itt_rfun.ml
+1 -1	metaprl/theories/itt/itt_set.ml
+1 -1	metaprl/theories/itt/itt_soft.ml
+20 -2	metaprl/theories/itt/itt_squash.ml
+5 -1	metaprl/theories/itt/itt_squash.mli
+1 -1	metaprl/theories/itt/itt_srec.ml
+2 -1	metaprl/theories/itt/itt_struct.ml
+10 -10	metaprl/theories/itt/itt_struct.mli
+20 -2	metaprl/theories/itt/itt_subtype.ml
+5 -1	metaprl/theories/itt/itt_subtype.mli
+1 -1	metaprl/theories/itt/itt_test.ml
+1 -1	metaprl/theories/itt/itt_test.mli
+1 -1	metaprl/theories/itt/itt_union.ml
+1 -1	metaprl/theories/itt/itt_unit.ml
+1 -1	metaprl/theories/itt/itt_void.ml
+1 -1	metaprl/theories/itt/main.ml
+1 -1	metaprl/theories/lf/main.ml
Properties	metaprl/theories/ocaml
+1 -1	metaprl/theories/ocaml/ocaml_base_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_expr_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_me_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_mt_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_patt_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_sig_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_str_df.ml
+1 -1	metaprl/theories/ocaml/ocaml_type_df.ml
+1 -1	metaprl/theories/ocaml_sos/ocaml_base_sos.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
+1 -1	metaprl/theories/rewrite/rw_beta.ml
Properties	metaprl/theories/tactic
+3 -2	metaprl/theories/tactic/Makefile
+2 -4	metaprl/theories/tactic/conversionals.ml
+21 -21	metaprl/theories/tactic/conversionals.mli
Added	metaprl/theories/tactic/nltop.ml
Properties	metaprl/theories/tactic/nltop.ml
Added	metaprl/theories/tactic/nltop.mli
Properties	metaprl/theories/tactic/nltop.mli
+1 -1	metaprl/theories/tactic/perv.ml
+2 -2	metaprl/theories/tactic/rewrite_type.ml
+1 -1	metaprl/theories/tactic/rewrite_type.mli
+1 -1	metaprl/theories/tactic/sequent.ml
+1 -1	metaprl/theories/tactic/tactic_cache.ml
+1 -1	metaprl/theories/tactic/tactic_type.ml
+1 -1	metaprl/theories/tactic/tactic_type.mli
+2 -1	metaprl/theories/tactic/tacticals.ml
+64 -63	metaprl/theories/tactic/tacticals.mli
+2 -2	metaprl/theories/tactic/var.ml
+1 -0	metaprl/util/ocamldep.mll