Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 1998-09-05 15:31:37 -0700 (Sat, 05 Sep 1998)
Revision: 2456
Log message:

      Added license headers to each of the files in preparation for
      the first major release.  The license is GNU public license; if
      any of you have problems with that, let me know right away.  When
      you add new code, you should credit yourself as the author.  When
      you modify code, you should add a "Modified by:" to the header,
      and possibly a short summary of your changes.
      
      I tried to get the Author lists as correct as I remember, but there
      are more than 550 files(!) and I may have made some mistakes. Please
      add yourself if I didn't do it right.
      

Changes  Path
Added metaprl/doc/license.html
Properties metaprl/doc/license.html
+28 -0 metaprl/editor/ml/czf.ml
+28 -0 metaprl/editor/ml/io_proof.ml
+28 -0 metaprl/editor/ml/io_proof.mli
+28 -0 metaprl/editor/ml/io_proof_type.mlz
+28 -0 metaprl/editor/ml/nl.ml
+28 -0 metaprl/editor/ml/nl.mli
+28 -0 metaprl/editor/ml/nl_top.ml
+28 -0 metaprl/editor/ml/nl_top.mli
+28 -0 metaprl/editor/ml/nl_version.mli
+28 -0 metaprl/editor/ml/package_df.ml
+28 -0 metaprl/editor/ml/package_df.mli
+28 -0 metaprl/editor/ml/package_info.ml
+28 -0 metaprl/editor/ml/package_info.mli
+28 -0 metaprl/editor/ml/package_int.ml
+28 -0 metaprl/editor/ml/package_int.mli
+28 -0 metaprl/editor/ml/package_type.mlz
+28 -0 metaprl/editor/ml/proof.ml
+28 -0 metaprl/editor/ml/proof.mli
+28 -0 metaprl/editor/ml/proof_edit.ml
+28 -0 metaprl/editor/ml/proof_edit.mli
+28 -0 metaprl/editor/ml/proof_step.ml
+28 -0 metaprl/editor/ml/proof_step.mli
+28 -0 metaprl/editor/ml/proof_type.mlz
+28 -0 metaprl/editor/ml/shell.ml
+28 -0 metaprl/editor/ml/shell.mli
+28 -0 metaprl/editor/ml/shell_nl.ml
+28 -0 metaprl/editor/ml/shell_nl.mli
+28 -0 metaprl/editor/ml/shell_null.ml
+28 -0 metaprl/editor/ml/shell_null.mli
+28 -0 metaprl/editor/ml/shell_p4.ml
+28 -0 metaprl/editor/ml/shell_p4.mli
+28 -0 metaprl/editor/ml/shell_p4_type.mlz
+28 -0 metaprl/editor/ml/shell_rewrite.ml
+28 -0 metaprl/editor/ml/shell_rewrite.mli
+28 -0 metaprl/editor/ml/shell_rule.ml
+28 -0 metaprl/editor/ml/shell_rule.mli
+28 -0 metaprl/editor/ml/shell_type.mlz
+28 -0 metaprl/editor/ml/test.ml
+28 -0 metaprl/editor/ml/test.mli
+28 -0 metaprl/editor/ml/w.ml
+28 -0 metaprl/editor/ml/x.ml
+28 -0 metaprl/editor/ml/y.ml
+28 -0 metaprl/editor/ml/z.ml
+28 -0 metaprl/ensemble/appl_closure.ml
+28 -0 metaprl/ensemble/appl_closure.mli
+28 -0 metaprl/ensemble/ensemble_queue.ml
+28 -0 metaprl/ensemble/ensemble_queue.mli
+28 -0 metaprl/ensemble/remote_ensemble.ml
+28 -0 metaprl/ensemble/remote_ensemble.mli
+28 -0 metaprl/ensemble/remote_null.ml
+28 -0 metaprl/ensemble/remote_null.mli
+28 -0 metaprl/ensemble/remote_sig.mlz
+28 -0 metaprl/ensemble/thread_refiner.mli
+28 -0 metaprl/ensemble/thread_refiner_ens.ml
+28 -0 metaprl/ensemble/thread_refiner_ens.mli
+28 -0 metaprl/ensemble/thread_refiner_ens_mod.ml
+28 -0 metaprl/ensemble/thread_refiner_null.ml
+28 -0 metaprl/ensemble/thread_refiner_null.mli
+28 -0 metaprl/ensemble/thread_refiner_null_mod.ml
+28 -0 metaprl/ensemble/thread_refiner_sig.mlz
+28 -0 metaprl/filter/filter_ast.ml
+28 -0 metaprl/filter/filter_ast.mli
+28 -0 metaprl/filter/filter_bin.ml
+28 -0 metaprl/filter/filter_bin.mli
+28 -0 metaprl/filter/filter_buffer.ml
+28 -0 metaprl/filter/filter_buffer.mli
+28 -0 metaprl/filter/filter_cache.ml
+28 -0 metaprl/filter/filter_cache.mli
+28 -0 metaprl/filter/filter_cache_fun.ml
+28 -0 metaprl/filter/filter_cache_fun.mli
+28 -0 metaprl/filter/filter_comment.ml
+28 -0 metaprl/filter/filter_comment.mli
+28 -0 metaprl/filter/filter_debug.ml
+28 -0 metaprl/filter/filter_debug.mli
+28 -0 metaprl/filter/filter_exn.ml
+28 -0 metaprl/filter/filter_exn.mli
+28 -0 metaprl/filter/filter_grammar.ml
+28 -0 metaprl/filter/filter_grammar.mli
+28 -0 metaprl/filter/filter_hash.ml
+28 -0 metaprl/filter/filter_hash.mli
+28 -0 metaprl/filter/filter_html.ml
+28 -0 metaprl/filter/filter_html.mli
+28 -0 metaprl/filter/filter_magic.mli
+28 -0 metaprl/filter/filter_main.ml
+28 -0 metaprl/filter/filter_main.mli
+28 -0 metaprl/filter/filter_ocaml.ml
+28 -0 metaprl/filter/filter_ocaml.mli
+28 -0 metaprl/filter/filter_parse.ml
+28 -0 metaprl/filter/filter_parse.mli
+28 -0 metaprl/filter/filter_prog.ml
+28 -0 metaprl/filter/filter_prog.mli
+28 -0 metaprl/filter/filter_summary.ml
+28 -0 metaprl/filter/filter_summary.mli
+28 -0 metaprl/filter/filter_summary_io.ml
+28 -0 metaprl/filter/filter_summary_io.mli
+28 -0 metaprl/filter/filter_summary_param.mlz
+28 -0 metaprl/filter/filter_summary_type.mlz
+28 -0 metaprl/filter/filter_summary_util.ml
+28 -0 metaprl/filter/filter_summary_util.mli
+28 -0 metaprl/filter/filter_type.mlz
+28 -0 metaprl/filter/filter_util.ml
+28 -0 metaprl/filter/filter_util.mli
+28 -0 metaprl/filter/free_vars.ml
+28 -0 metaprl/filter/free_vars.mli
+28 -0 metaprl/filter/infix.mli
+28 -0 metaprl/filter/infix.pre.ml
+28 -0 metaprl/filter/mLast_util.ml
+28 -0 metaprl/filter/mLast_util.mli
+28 -0 metaprl/filter/prlcomp.ml
+28 -0 metaprl/filter/prlcomp.mli
+28 -0 metaprl/filter/term_grammar.ml
+28 -0 metaprl/filter/term_grammar.mli
+28 -0 metaprl/filter/term_quote.ml
+28 -0 metaprl/filter/term_quote.mli
+28 -0 metaprl/filter/test.ml
+28 -0 metaprl/filter/test.mli
+28 -0 metaprl/filter/test_filter.ml
+28 -0 metaprl/filter/test_filter.mli
+28 -0 metaprl/filter/test_gram.ml
+28 -0 metaprl/horus/opname.ml
+28 -0 metaprl/horus/opname.mli
+28 -0 metaprl/horus/term.ml
+28 -0 metaprl/horus/term.mli
+28 -0 metaprl/horus/util.ml
+28 -0 metaprl/horus/util.mli
+26 -0 metaprl/library/ascii_scan.ml
+26 -0 metaprl/library/ascii_scan.mli
+26 -0 metaprl/library/basic.ml
+26 -0 metaprl/library/basic.mli
+26 -0 metaprl/library/bigInt.ml
+26 -0 metaprl/library/bigInt.mli
+26 -0 metaprl/library/db.ml
+26 -0 metaprl/library/db.mli
+26 -0 metaprl/library/definition.ml
+26 -0 metaprl/library/definition.mli
+26 -0 metaprl/library/int32.ml
+26 -0 metaprl/library/int32.mli
+26 -0 metaprl/library/library.ml
+26 -0 metaprl/library/library.mli
+26 -0 metaprl/library/library_eval.ml
+26 -0 metaprl/library/library_eval.mli
+26 -0 metaprl/library/library_type_base.mli
+26 -0 metaprl/library/link.mli
+26 -0 metaprl/library/mathBus.ml
+26 -0 metaprl/library/mathBus.mli
+26 -0 metaprl/library/mbterm.ml
+26 -0 metaprl/library/mbterm.mli
+26 -0 metaprl/library/nuprl5.ml
+26 -0 metaprl/library/nuprl5.mli
+26 -0 metaprl/library/object_id.ml
+26 -0 metaprl/library/object_id.mli
+26 -0 metaprl/library/oidtable.ml
+26 -0 metaprl/library/oidtable.mli
+26 -0 metaprl/library/orb.ml
+26 -0 metaprl/library/orb.mli
+25 -0 metaprl/library/registry.ml
+26 -0 metaprl/library/registry.mli
+26 -0 metaprl/library/socketIo.ml
+26 -0 metaprl/library/socketIo.mli
+26 -0 metaprl/library/tentfunctor.ml
+26 -0 metaprl/library/tentfunctor.mli
+24 -0 metaprl/library/test.ml
+26 -0 metaprl/library/utils.ml
+26 -0 metaprl/library/utils.mli
+28 -0 metaprl/mllib/cycle_dag.ml
+28 -0 metaprl/mllib/cycle_dag.mli
+28 -0 metaprl/mllib/dag.mlz
+27 -0 metaprl/mllib/debug_string_sets.mli
+28 -0 metaprl/mllib/env_arg.mli
+28 -0 metaprl/mllib/file_base.ml
+28 -0 metaprl/mllib/file_base.mli
+28 -0 metaprl/mllib/file_base_type.ml
+28 -0 metaprl/mllib/file_type_base.ml
+28 -0 metaprl/mllib/file_type_base.mli
+28 -0 metaprl/mllib/file_util.ml
+28 -0 metaprl/mllib/file_util.mli
+28 -0 metaprl/mllib/filename_util.ml
+28 -0 metaprl/mllib/filename_util.mli
+28 -0 metaprl/mllib/flist.ml
+28 -0 metaprl/mllib/flist.mli
+27 -0 metaprl/mllib/fun_splay_set.ml
+27 -0 metaprl/mllib/fun_splay_set.mli
+28 -0 metaprl/mllib/getrusage.ml
+28 -0 metaprl/mllib/getrusage.mli
+28 -0 metaprl/mllib/hash_set.ml
+28 -0 metaprl/mllib/hash_set.mli
+28 -0 metaprl/mllib/imp_dag.ml
+28 -0 metaprl/mllib/imp_dag.mli
+28 -0 metaprl/mllib/list_util.ml
+28 -0 metaprl/mllib/list_util.mli
+28 -0 metaprl/mllib/memo.ml
+28 -0 metaprl/mllib/memo.mli
+28 -0 metaprl/mllib/nl_big_int.ml
+28 -0 metaprl/mllib/nl_big_int.mli
+28 -0 metaprl/mllib/nl_debug.ml
+28 -0 metaprl/mllib/nl_debug.mli
+28 -0 metaprl/mllib/nl_num.ml
+28 -0 metaprl/mllib/nl_num.mli
+28 -0 metaprl/mllib/nl_pervasives.ml
+28 -0 metaprl/mllib/nl_pervasives.mli
+27 -0 metaprl/mllib/nl_set.mlz
+28 -0 metaprl/mllib/precedence.ml
+28 -0 metaprl/mllib/precedence.mli
+28 -0 metaprl/mllib/punix.ml
+28 -0 metaprl/mllib/punix.mli
+28 -0 metaprl/mllib/red_black_set.ml
+28 -0 metaprl/mllib/red_black_set.mli
+28 -0 metaprl/mllib/red_black_test.ml
+28 -0 metaprl/mllib/red_black_test.mli
+28 -0 metaprl/mllib/ref_util.ml
+28 -0 metaprl/mllib/ref_util.mli
+28 -0 metaprl/mllib/remote_lazy_queue.ml
+28 -0 metaprl/mllib/remote_lazy_queue.mli
+28 -0 metaprl/mllib/remote_lazy_queue_sig.ml
+28 -0 metaprl/mllib/remote_queue_null.ml
+28 -0 metaprl/mllib/remote_queue_null.mli
+28 -0 metaprl/mllib/remote_queue_sig.ml
+28 -0 metaprl/mllib/small_set.ml
+28 -0 metaprl/mllib/small_set.mli
+28 -0 metaprl/mllib/splay_table.ml
+28 -0 metaprl/mllib/splay_table.mli
+28 -0 metaprl/mllib/string_set.ml
+28 -0 metaprl/mllib/string_set.mli
+28 -0 metaprl/mllib/string_util.ml
+28 -0 metaprl/mllib/string_util.mli
+28 -0 metaprl/mllib/thread_event.ml
+28 -0 metaprl/mllib/thread_event.mli
+28 -0 metaprl/mllib/thread_util.ml
+28 -0 metaprl/mllib/thread_util.mli
+28 -0 metaprl/mllib/unix_util.ml
+28 -0 metaprl/mllib/unix_util.mli
+28 -0 metaprl/refiner/refbase/opname.ml
+28 -0 metaprl/refiner/refbase/opname.mli
+28 -0 metaprl/refiner/refiner/refine.mlip
+28 -0 metaprl/refiner/refiner/refine.mlp
+28 -0 metaprl/refiner/refiner/refine_error.ml
+28 -0 metaprl/refiner/refiner/refine_error.mli
+28 -0 metaprl/refiner/refiner/refiner.ml
+28 -0 metaprl/refiner/refiner/refiner.mli
+28 -0 metaprl/refiner/refiner/refiner_ds_simp.ml
+28 -0 metaprl/refiner/refiner/refiner_ds_simp.mli
+28 -0 metaprl/refiner/refiner/refiner_ds_verb.ml
+28 -0 metaprl/refiner/refiner/refiner_ds_verb.mli
+28 -0 metaprl/refiner/refiner/refiner_std_simp.ml
+28 -0 metaprl/refiner/refiner/refiner_std_simp.mli
+28 -0 metaprl/refiner/refiner/refiner_std_verb.ml
+28 -0 metaprl/refiner/refiner/refiner_std_verb.mli
+28 -0 metaprl/refiner/reflib/dform.ml
+28 -0 metaprl/refiner/reflib/dform.mli
+28 -0 metaprl/refiner/reflib/dform_print.ml
+28 -0 metaprl/refiner/reflib/dform_print.mli
+28 -0 metaprl/refiner/reflib/ml_file.ml
+28 -0 metaprl/refiner/reflib/ml_file.mli
+28 -0 metaprl/refiner/reflib/ml_format.ml
+28 -0 metaprl/refiner/reflib/ml_format.mli
+28 -0 metaprl/refiner/reflib/ml_format_sig.mlz
+28 -0 metaprl/refiner/reflib/ml_print.ml
+28 -0 metaprl/refiner/reflib/ml_print.mli
+28 -0 metaprl/refiner/reflib/ml_print_sig.mlz
+28 -0 metaprl/refiner/reflib/ml_string.ml
+28 -0 metaprl/refiner/reflib/ml_string.mli
+28 -0 metaprl/refiner/reflib/ml_term.ml
+28 -0 metaprl/refiner/reflib/ml_term.mli
+28 -0 metaprl/refiner/reflib/nl_resource.ml
+28 -0 metaprl/refiner/reflib/nl_resource.mli
+28 -0 metaprl/refiner/reflib/refine_exn.ml
+28 -0 metaprl/refiner/reflib/refine_exn.mli
+28 -0 metaprl/refiner/reflib/rformat.ml
+28 -0 metaprl/refiner/reflib/rformat.mli
+28 -0 metaprl/refiner/reflib/simple_print.ml
+28 -0 metaprl/refiner/reflib/simple_print.mli
+28 -0 metaprl/refiner/reflib/simple_print_sig.ml
+28 -0 metaprl/refiner/reflib/term_copy.ml
+28 -0 metaprl/refiner/reflib/term_copy.mli
+28 -0 metaprl/refiner/reflib/term_dtable.ml
+28 -0 metaprl/refiner/reflib/term_dtable.mli
+28 -0 metaprl/refiner/reflib/term_stable.ml
+28 -0 metaprl/refiner/reflib/term_stable.mli
+28 -0 metaprl/refiner/reflib/term_table.ml
+28 -0 metaprl/refiner/reflib/term_table.mli
+28 -0 metaprl/refiner/reflib/theory.ml
+28 -0 metaprl/refiner/reflib/theory.mli
+28 -0 metaprl/refiner/refsig/refine_error_sig.ml
+28 -0 metaprl/refiner/refsig/refine_sig.ml
+28 -0 metaprl/refiner/refsig/refiner_sig.ml
+28 -0 metaprl/refiner/refsig/resource.mlz
+28 -0 metaprl/refiner/refsig/rewrite_sig.ml
+28 -0 metaprl/refiner/refsig/term_addr_sig.ml
+28 -0 metaprl/refiner/refsig/term_base_sig.ml
+28 -0 metaprl/refiner/refsig/term_eval_sig.ml
+28 -0 metaprl/refiner/refsig/term_man_sig.ml
+28 -0 metaprl/refiner/refsig/term_meta_sig.ml
+28 -0 metaprl/refiner/refsig/term_op_sig.ml
+28 -0 metaprl/refiner/refsig/term_shape_sig.ml
+28 -0 metaprl/refiner/refsig/term_simple_sig.mlz
+28 -0 metaprl/refiner/refsig/term_subst_sig.ml
+28 -0 metaprl/refiner/rewrite/rewrite.mlip
+28 -0 metaprl/refiner/rewrite/rewrite.mlp
+28 -0 metaprl/refiner/rewrite/rewrite_build_contractum.mlip
+28 -0 metaprl/refiner/rewrite/rewrite_build_contractum.mlp
+28 -0 metaprl/refiner/rewrite/rewrite_build_contractum_sig.mlz
+28 -0 metaprl/refiner/rewrite/rewrite_compile_contractum.mlip
+28 -0 metaprl/refiner/rewrite/rewrite_compile_contractum.mlp
+28 -0 metaprl/refiner/rewrite/rewrite_compile_contractum_sig.mlz
+28 -0 metaprl/refiner/rewrite/rewrite_compile_redex.mlip
+28 -0 metaprl/refiner/rewrite/rewrite_compile_redex.mlp
+28 -0 metaprl/refiner/rewrite/rewrite_compile_redex_sig.mlz
+28 -0 metaprl/refiner/rewrite/rewrite_debug.mlip
+28 -0 metaprl/refiner/rewrite/rewrite_debug.mlp
+28 -0 metaprl/refiner/rewrite/rewrite_debug_sig.ml
+28 -0 metaprl/refiner/rewrite/rewrite_match_redex.mlip
+28 -0 metaprl/refiner/rewrite/rewrite_match_redex.mlp
+28 -0 metaprl/refiner/rewrite/rewrite_match_redex_sig.mlz
+28 -0 metaprl/refiner/rewrite/rewrite_meta.mlip
+28 -0 metaprl/refiner/rewrite/rewrite_meta.mlp
+28 -0 metaprl/refiner/rewrite/rewrite_meta_sig.mlz
+28 -0 metaprl/refiner/rewrite/rewrite_type.mlip
+28 -0 metaprl/refiner/rewrite/rewrite_type.mlp
+28 -0 metaprl/refiner/rewrite/rewrite_type_sig.mlz
+28 -0 metaprl/refiner/rewrite/rewrite_util.mlip
+28 -0 metaprl/refiner/rewrite/rewrite_util.mlp
+28 -0 metaprl/refiner/rewrite/rewrite_util_sig.ml
+26 -0 metaprl/refiner/term_ds/term_addr_ds.mlip
+26 -0 metaprl/refiner/term_ds/term_addr_ds.mlp
+26 -0 metaprl/refiner/term_ds/term_base_ds.mlip
+26 -0 metaprl/refiner/term_ds/term_base_ds.mlp
+28 -0 metaprl/refiner/term_ds/term_ds.ml
+28 -0 metaprl/refiner/term_ds/term_ds.mli
+28 -0 metaprl/refiner/term_ds/term_ds_sig.ml
+26 -0 metaprl/refiner/term_ds/term_eval_ds.mlip
+26 -0 metaprl/refiner/term_ds/term_eval_ds.mlp
+26 -0 metaprl/refiner/term_ds/term_man_ds.mlip
+26 -0 metaprl/refiner/term_ds/term_man_ds.mlp
+26 -0 metaprl/refiner/term_ds/term_op_ds.mlip
+26 -0 metaprl/refiner/term_ds/term_op_ds.mlp
+26 -0 metaprl/refiner/term_ds/term_subst_ds.mlip
+27 -0 metaprl/refiner/term_ds/term_subst_ds.mlp
+27 -0 metaprl/refiner/term_gen/term_addr_gen.mlip
+27 -0 metaprl/refiner/term_gen/term_man_gen.mlip
+28 -0 metaprl/refiner/term_gen/term_man_gen.mlp
+28 -0 metaprl/refiner/term_gen/term_meta_gen.mlip
+28 -0 metaprl/refiner/term_gen/term_meta_gen.mlp
+28 -0 metaprl/refiner/term_gen/term_shape_gen.mlip
+28 -0 metaprl/refiner/term_gen/term_shape_gen.mlp
+28 -0 metaprl/refiner/term_std/term_base_std.mlip
+28 -0 metaprl/refiner/term_std/term_base_std.mlp
+28 -0 metaprl/refiner/term_std/term_eval_std.mlip
+26 -0 metaprl/refiner/term_std/term_eval_std.mlp
+28 -0 metaprl/refiner/term_std/term_op_std.mlip
+28 -0 metaprl/refiner/term_std/term_op_std.mlp
+28 -0 metaprl/refiner/term_std/term_std.ml
+28 -0 metaprl/refiner/term_std/term_std.mli
+28 -0 metaprl/refiner/term_std/term_std_sig.ml
+28 -0 metaprl/refiner/term_std/term_subst_std.mlip
+28 -0 metaprl/refiner/term_std/term_subst_std.mlp
+28 -0 metaprl/theories/base/base_auto_tactic.ml
+28 -0 metaprl/theories/base/base_auto_tactic.mli
+28 -0 metaprl/theories/base/base_cache.ml
+28 -0 metaprl/theories/base/base_cache.mli
+28 -0 metaprl/theories/base/base_dform.ml
+28 -0 metaprl/theories/base/base_dform.mli
+28 -0 metaprl/theories/base/base_dtactic.ml
+28 -0 metaprl/theories/base/base_dtactic.mli
+28 -0 metaprl/theories/base/base_rewrite.ml
+28 -0 metaprl/theories/base/base_rewrite.mli
+28 -0 metaprl/theories/base/base_theory.mlz
+28 -0 metaprl/theories/base/nuprl_font.ml
+28 -0 metaprl/theories/base/nuprl_font.mli
+28 -0 metaprl/theories/base/summary.ml
+28 -0 metaprl/theories/base/summary.mli
+28 -0 metaprl/theories/base/typeinf.ml
+28 -0 metaprl/theories/base/typeinf.mli
+28 -0 metaprl/theories/caml/caml_syntax.mli
+28 -0 metaprl/theories/czf/czf_all.mli
+28 -0 metaprl/theories/czf/czf_and.mli
+28 -0 metaprl/theories/czf/czf_equal.mli
+28 -0 metaprl/theories/czf/czf_exists.mli
+28 -0 metaprl/theories/czf/czf_false.mli
+28 -0 metaprl/theories/czf/czf_implies.mli
+28 -0 metaprl/theories/czf/czf_itt_all.ml
+28 -0 metaprl/theories/czf/czf_itt_all.mli
+28 -0 metaprl/theories/czf/czf_itt_and.ml
+28 -0 metaprl/theories/czf/czf_itt_and.mli
+28 -0 metaprl/theories/czf/czf_itt_axioms.ml
+28 -0 metaprl/theories/czf/czf_itt_axioms.mli
+28 -0 metaprl/theories/czf/czf_itt_dall.ml
+28 -0 metaprl/theories/czf/czf_itt_dall.mli
+28 -0 metaprl/theories/czf/czf_itt_dexists.ml
+28 -0 metaprl/theories/czf/czf_itt_dexists.mli
+28 -0 metaprl/theories/czf/czf_itt_empty.ml
+28 -0 metaprl/theories/czf/czf_itt_empty.mli
+28 -0 metaprl/theories/czf/czf_itt_eq.ml
+28 -0 metaprl/theories/czf/czf_itt_eq.mli
+28 -0 metaprl/theories/czf/czf_itt_eq_inner.ml
+28 -0 metaprl/theories/czf/czf_itt_eq_inner.mli
+28 -0 metaprl/theories/czf/czf_itt_exists.ml
+28 -0 metaprl/theories/czf/czf_itt_exists.mli
+28 -0 metaprl/theories/czf/czf_itt_false.ml
+28 -0 metaprl/theories/czf/czf_itt_false.mli
+28 -0 metaprl/theories/czf/czf_itt_implies.ml
+28 -0 metaprl/theories/czf/czf_itt_implies.mli
+28 -0 metaprl/theories/czf/czf_itt_isect.mli
+28 -0 metaprl/theories/czf/czf_itt_member.ml
+28 -0 metaprl/theories/czf/czf_itt_member.mli
+28 -0 metaprl/theories/czf/czf_itt_or.ml
+28 -0 metaprl/theories/czf/czf_itt_or.mli
+28 -0 metaprl/theories/czf/czf_itt_pre_set.ml
+28 -0 metaprl/theories/czf/czf_itt_pre_set.mli
+28 -0 metaprl/theories/czf/czf_itt_rel.ml
+28 -0 metaprl/theories/czf/czf_itt_rel.mli
+28 -0 metaprl/theories/czf/czf_itt_res.ml
+28 -0 metaprl/theories/czf/czf_itt_res.mli
+28 -0 metaprl/theories/czf/czf_itt_sall.ml
+28 -0 metaprl/theories/czf/czf_itt_sall.mli
+28 -0 metaprl/theories/czf/czf_itt_sep.ml
+28 -0 metaprl/theories/czf/czf_itt_sep.mli
+28 -0 metaprl/theories/czf/czf_itt_set.ml
+28 -0 metaprl/theories/czf/czf_itt_set.mli
+28 -0 metaprl/theories/czf/czf_itt_set_ext.ml
+28 -0 metaprl/theories/czf/czf_itt_set_ext.mli
+28 -0 metaprl/theories/czf/czf_itt_set_ind.ml
+28 -0 metaprl/theories/czf/czf_itt_set_ind.mli
+28 -0 metaprl/theories/czf/czf_itt_sexists.ml
+28 -0 metaprl/theories/czf/czf_itt_sexists.mli
+28 -0 metaprl/theories/czf/czf_itt_small.ml
+28 -0 metaprl/theories/czf/czf_itt_small.mli
+28 -0 metaprl/theories/czf/czf_itt_true.ml
+28 -0 metaprl/theories/czf/czf_itt_true.mli
+28 -0 metaprl/theories/czf/czf_itt_union.ml
+28 -0 metaprl/theories/czf/czf_itt_union.mli
+28 -0 metaprl/theories/czf/czf_member.mli
+28 -0 metaprl/theories/czf/czf_or.mli
+28 -0 metaprl/theories/czf/czf_set.ml
+28 -0 metaprl/theories/czf/czf_set.mli
+28 -0 metaprl/theories/czf/czf_struct.mli
+28 -0 metaprl/theories/czf/czf_theory.mli
+28 -0 metaprl/theories/czf/czf_true.ml
+28 -0 metaprl/theories/czf/czf_true.mli
+28 -0 metaprl/theories/czf/czf_wf.ml
+28 -0 metaprl/theories/czf/czf_wf.mli
+28 -0 metaprl/theories/itt/itt_arith.ml
+28 -0 metaprl/theories/itt/itt_arith.mli
+28 -0 metaprl/theories/itt/itt_atom.ml
+28 -0 metaprl/theories/itt/itt_atom.mli
+28 -0 metaprl/theories/itt/itt_bool.ml
+28 -0 metaprl/theories/itt/itt_bool.mli
+28 -0 metaprl/theories/itt/itt_derive.ml
+28 -0 metaprl/theories/itt/itt_derive.mli
+28 -0 metaprl/theories/itt/itt_dfun.ml
+28 -0 metaprl/theories/itt/itt_dfun.mli
+28 -0 metaprl/theories/itt/itt_dprod.ml
+28 -0 metaprl/theories/itt/itt_dprod.mli
+28 -0 metaprl/theories/itt/itt_equal.ml
+28 -0 metaprl/theories/itt/itt_equal.mli
+28 -0 metaprl/theories/itt/itt_ext_equal.ml
+28 -0 metaprl/theories/itt/itt_ext_equal.mli
+28 -0 metaprl/theories/itt/itt_fun.ml
+28 -0 metaprl/theories/itt/itt_fun.mli
+28 -0 metaprl/theories/itt/itt_int.ml
+28 -0 metaprl/theories/itt/itt_int.mli
+28 -0 metaprl/theories/itt/itt_int_bool.ml
+28 -0 metaprl/theories/itt/itt_int_bool.mli
+28 -0 metaprl/theories/itt/itt_isect.ml
+28 -0 metaprl/theories/itt/itt_isect.mli
+28 -0 metaprl/theories/itt/itt_list.ml
+28 -0 metaprl/theories/itt/itt_list.mli
+28 -0 metaprl/theories/itt/itt_logic.ml
+28 -0 metaprl/theories/itt/itt_logic.mli
+28 -0 metaprl/theories/itt/itt_prec.ml
+28 -0 metaprl/theories/itt/itt_prec.mli
+28 -0 metaprl/theories/itt/itt_prod.ml
+28 -0 metaprl/theories/itt/itt_prod.mli
+28 -0 metaprl/theories/itt/itt_prop_decide.ml
+28 -0 metaprl/theories/itt/itt_prop_decide.mli
+28 -0 metaprl/theories/itt/itt_quotient.ml
+28 -0 metaprl/theories/itt/itt_quotient.mli
+28 -0 metaprl/theories/itt/itt_rfun.ml
+28 -0 metaprl/theories/itt/itt_rfun.mli
+28 -0 metaprl/theories/itt/itt_set.ml
+28 -0 metaprl/theories/itt/itt_set.mli
+28 -0 metaprl/theories/itt/itt_squash.ml
+28 -0 metaprl/theories/itt/itt_squash.mli
+28 -0 metaprl/theories/itt/itt_srec.ml
+28 -0 metaprl/theories/itt/itt_srec.mli
+28 -0 metaprl/theories/itt/itt_struct.ml
+28 -0 metaprl/theories/itt/itt_struct.mli
+28 -0 metaprl/theories/itt/itt_subtype.ml
+28 -0 metaprl/theories/itt/itt_subtype.mli
+28 -0 metaprl/theories/itt/itt_test.ml
+28 -0 metaprl/theories/itt/itt_test.mli
+28 -0 metaprl/theories/itt/itt_theory.ml
+28 -0 metaprl/theories/itt/itt_theory.mli
+28 -0 metaprl/theories/itt/itt_union.ml
+28 -0 metaprl/theories/itt/itt_union.mli
+28 -0 metaprl/theories/itt/itt_unit.ml
+28 -0 metaprl/theories/itt/itt_unit.mli
+28 -0 metaprl/theories/itt/itt_void.ml
+28 -0 metaprl/theories/itt/itt_void.mli
+28 -0 metaprl/theories/itt/itt_w.ml
+28 -0 metaprl/theories/itt/itt_w.mli
+28 -0 metaprl/theories/itt/main.ml
+28 -0 metaprl/theories/itt/main.mli
+28 -0 metaprl/theories/itt/test.ml
+28 -0 metaprl/theories/itt/test.mli
+28 -0 metaprl/theories/lf/lf_ctx.mli
+28 -0 metaprl/theories/lf/lf_dfun.mli
+28 -0 metaprl/theories/lf/lf_kind.mli
+28 -0 metaprl/theories/lf/lf_sig.mli
+28 -0 metaprl/theories/lf/lf_type.mli
+28 -0 metaprl/theories/lf/main.ml
+28 -0 metaprl/theories/ocaml/ocaml.mlz
+28 -0 metaprl/theories/ocaml/ocaml_base_df.ml
+28 -0 metaprl/theories/ocaml/ocaml_base_df.mli
+28 -0 metaprl/theories/ocaml/ocaml_df.mlz
+28 -0 metaprl/theories/ocaml/ocaml_expr_df.ml
+28 -0 metaprl/theories/ocaml/ocaml_expr_df.mli
+28 -0 metaprl/theories/ocaml/ocaml_me_df.ml
+28 -0 metaprl/theories/ocaml/ocaml_me_df.mli
+28 -0 metaprl/theories/ocaml/ocaml_mt_df.ml
+28 -0 metaprl/theories/ocaml/ocaml_mt_df.mli
+28 -0 metaprl/theories/ocaml/ocaml_patt_df.ml
+28 -0 metaprl/theories/ocaml/ocaml_patt_df.mli
+28 -0 metaprl/theories/ocaml/ocaml_sig_df.ml
+28 -0 metaprl/theories/ocaml/ocaml_sig_df.mli
+28 -0 metaprl/theories/ocaml/ocaml_str_df.ml
+28 -0 metaprl/theories/ocaml/ocaml_str_df.mli
+28 -0 metaprl/theories/ocaml/ocaml_type_df.ml
+28 -0 metaprl/theories/ocaml/ocaml_type_df.mli
+28 -0 metaprl/theories/ocaml_sos/ocaml_base_sos.ml
+28 -0 metaprl/theories/ocaml_sos/ocaml_base_sos.mli
+28 -0 metaprl/theories/ocaml_sos/ocaml_expr_sos.ml
+28 -0 metaprl/theories/ocaml_sos/ocaml_expr_sos.mli
+28 -0 metaprl/theories/ocaml_sos/ocaml_logic.ml
+28 -0 metaprl/theories/ocaml_sos/ocaml_logic.mli
+28 -0 metaprl/theories/ocaml_sos/ocaml_me_sos.ml
+28 -0 metaprl/theories/ocaml_sos/ocaml_me_sos.mli
+28 -0 metaprl/theories/ocaml_sos/ocaml_mt_sos.ml
+28 -0 metaprl/theories/ocaml_sos/ocaml_mt_sos.mli
+28 -0 metaprl/theories/ocaml_sos/ocaml_patt_sos.ml
+28 -0 metaprl/theories/ocaml_sos/ocaml_patt_sos.mli
+28 -0 metaprl/theories/ocaml_sos/ocaml_sig_sos.ml
+28 -0 metaprl/theories/ocaml_sos/ocaml_sig_sos.mli
+28 -0 metaprl/theories/ocaml_sos/ocaml_str_sos.ml
+28 -0 metaprl/theories/ocaml_sos/ocaml_str_sos.mli
+28 -0 metaprl/theories/ocaml_sos/ocaml_theory.mlz
+28 -0 metaprl/theories/ocaml_sos/ocaml_type_sos.ml
+28 -0 metaprl/theories/ocaml_sos/ocaml_type_sos.mli
+28 -0 metaprl/theories/rewrite/rw_beta.ml
+28 -0 metaprl/theories/rewrite/rw_beta.mli
+28 -0 metaprl/theories/tactic/conversionals.ml
+28 -0 metaprl/theories/tactic/conversionals.mli
+28 -0 metaprl/theories/tactic/nltop.ml
+28 -0 metaprl/theories/tactic/nltop.mli
+28 -0 metaprl/theories/tactic/perv.ml
+28 -0 metaprl/theories/tactic/perv.mli
+28 -0 metaprl/theories/tactic/remote_null.ml
+28 -0 metaprl/theories/tactic/remote_null.mli
+28 -0 metaprl/theories/tactic/remote_sig.mlz
+28 -0 metaprl/theories/tactic/rewrite_type.ml
+28 -0 metaprl/theories/tactic/rewrite_type.mli
+28 -0 metaprl/theories/tactic/sequent.ml
+28 -0 metaprl/theories/tactic/sequent.mli
+28 -0 metaprl/theories/tactic/tactic_cache.ml
+28 -0 metaprl/theories/tactic/tactic_cache.mli
+28 -0 metaprl/theories/tactic/tactic_type.ml
+28 -0 metaprl/theories/tactic/tactic_type.mli
+28 -0 metaprl/theories/tactic/tacticals.ml
+28 -0 metaprl/theories/tactic/tacticals.mli
+28 -0 metaprl/theories/tactic/var.ml
+28 -0 metaprl/theories/tactic/var.mli
+28 -0 metaprl/theories/tptp/tptp.mli
+28 -0 metaprl/theories/tptp/tptp_cache.ml
+28 -0 metaprl/theories/tptp/tptp_cache.mli
+28 -0 metaprl/theories/tptp/tptp_lex.mli
+28 -0 metaprl/theories/tptp/tptp_load.ml
+28 -0 metaprl/theories/tptp/tptp_load.mli
+28 -0 metaprl/theories/tptp/tptp_prove.ml
+28 -0 metaprl/theories/tptp/tptp_prove.mli
+28 -0 metaprl/theories/tptp/tptp_type.mlz