/[mojave]
ViewVC logotype

Revision 2443


Jump to revision: Previous Next
Author: jyh
Date: Mon Aug 24 13:43:48 1998 UTC (22 years, 11 months ago)
Changed paths: 149 (showing only 100; show all)
Log Message:
Slightly better Ensemble scheduling.
Native-code compiler has trouble marshaling functions--
its probably a problem with the marshaler.

Added Nl_num, a ML-only implementation of bignums.
This is slower than the C version used by OCaml, but
we can marshal the Nl_nums.  Most of the files changed
are just replacements of Num.* with Nl_num.*.


Changed paths

Path Details
Directorymetaprl/editor/ml/.gdbinit added
Directorymetaprl/editor/ml/Makefile modified , text changed
Directorymetaprl/editor/ml/io_proof.ml modified , text changed
Directorymetaprl/editor/ml/nlconfig modified , text changed
Directorymetaprl/editor/ml/nlgossip modified , text changed
Directorymetaprl/editor/ml/nlopt modified , text changed
Directorymetaprl/editor/ml/package_info.ml modified , text changed
Directorymetaprl/editor/ml/shell_nl.ml modified , text changed
Directorymetaprl/editor/ml/shell_p4.ml modified , text changed
Directorymetaprl/ensemble/Makefile modified , text changed
Directorymetaprl/ensemble/ensemble_queue.ml modified , text changed
Directorymetaprl/ensemble/remote_ensemble.ml modified , text changed
Directorymetaprl/ensemble/remote_null.ml modified , text changed
Directorymetaprl/ensemble/remote_sig.mlz modified , text changed
Directorymetaprl/ensemble/thread_refiner_ens.ml modified , text changed
Directorymetaprl/ensemble/thread_refiner_null.ml modified , text changed
Directorymetaprl/ensemble/thread_refiner_sig.mlz modified , text changed
Directorymetaprl/filter/Makefile modified , text changed
Directorymetaprl/filter/buffer.ml deleted
Directorymetaprl/filter/buffer.mli deleted
Directorymetaprl/filter/filter_ast.ml modified , text changed
Directorymetaprl/filter/filter_buffer.ml added
Directorymetaprl/filter/filter_buffer.mli added
Directorymetaprl/filter/filter_cache_fun.ml modified , text changed
Directorymetaprl/filter/filter_comment.ml modified , text changed
Directorymetaprl/filter/filter_magic.ml modified , text changed
Directorymetaprl/filter/filter_main.ml modified , text changed
Directorymetaprl/filter/filter_ocaml.ml modified , text changed
Directorymetaprl/filter/filter_ocaml.mli modified , text changed
Directorymetaprl/filter/filter_parse.ml modified , text changed
Directorymetaprl/filter/filter_prog.ml modified , text changed
Directorymetaprl/filter/filter_summary.ml modified , text changed
Directorymetaprl/filter/filter_summary_util.ml modified , text changed
Directorymetaprl/filter/term_grammar.ml modified , text changed
Directorymetaprl/library/Makefile modified , text changed
Directorymetaprl/library/ascii_scan.ml modified , text changed
Directorymetaprl/library/ascii_scan.mli modified , text changed
Directorymetaprl/library/basic.ml modified , text changed
Directorymetaprl/library/basic.mli modified , text changed
Directorymetaprl/library/db.ml modified , text changed
Directorymetaprl/library/library_eval.ml modified , text changed
Directorymetaprl/library/link.ml modified , text changed
Directorymetaprl/library/mathBus.ml modified , text changed
Directorymetaprl/library/mathBus.mli modified , text changed
Directorymetaprl/library/mbterm.ml modified , text changed
Directorymetaprl/library/nuprl5.ml modified , text changed
Directorymetaprl/library/nuprl5.mli modified , text changed
Directorymetaprl/library/orb.ml modified , text changed
Directorymetaprl/library/registry.ml modified , text changed
Directorymetaprl/mllib/Makefile modified , text changed
Directorymetaprl/mllib/file_type_base.ml modified , text changed
Directorymetaprl/mllib/file_util.ml modified , text changed
Directorymetaprl/mllib/nl_big_int.ml added
Directorymetaprl/mllib/nl_big_int.mli added
Directorymetaprl/mllib/nl_num.ml added
Directorymetaprl/mllib/nl_num.mli added
Directorymetaprl/mllib/nl_pervasives.ml added
Directorymetaprl/mllib/nl_pervasives.mli added
Directorymetaprl/mllib/remote_lazy_queue.ml modified , text changed
Directorymetaprl/mllib/remote_lazy_queue_sig.ml modified , text changed
Directorymetaprl/mllib/remote_queue_null.ml modified , text changed
Directorymetaprl/mllib/remote_queue_sig.ml modified , text changed
Directorymetaprl/refiner/reflib/Files modified , text changed
Directorymetaprl/refiner/reflib/ml_format_sig.mlz modified , text changed
Directorymetaprl/refiner/reflib/ml_print.ml modified , text changed
Directorymetaprl/refiner/reflib/nl_resource.ml added
Directorymetaprl/refiner/reflib/nl_resource.mli added
Directorymetaprl/refiner/reflib/resource.ml deleted
Directorymetaprl/refiner/reflib/resource.mli deleted
Directorymetaprl/refiner/reflib/rformat.ml modified , text changed
Directorymetaprl/refiner/reflib/rformat.mli modified , text changed
Directorymetaprl/refiner/reflib/term_copy.ml modified , text changed
Directorymetaprl/refiner/refsig/term_op_sig.ml modified , text changed
Directorymetaprl/refiner/refsig/term_simple_sig.mlz modified , text changed
Directorymetaprl/refiner/rewrite/rewrite.mlp modified , text changed
Directorymetaprl/refiner/rewrite/rewrite_build_contractum.mlp modified , text changed
Directorymetaprl/refiner/rewrite/rewrite_debug.mlp modified , text changed
Directorymetaprl/refiner/rewrite/rewrite_match_redex.mlp modified , text changed
Directorymetaprl/refiner/rewrite/rewrite_type.mlp modified , text changed
Directorymetaprl/refiner/rewrite/rewrite_type_sig.mlz modified , text changed
Directorymetaprl/refiner/term_ds/term_ds.ml modified , text changed
Directorymetaprl/refiner/term_ds/term_ds_sig.ml modified , text changed
Directorymetaprl/refiner/term_ds/term_subst_ds.mlp modified , text changed
Directorymetaprl/refiner/term_std/term_std.ml modified , text changed
Directorymetaprl/refiner/term_std/term_std_sig.ml modified , text changed
Directorymetaprl/refiner/term_std/term_subst_std.mlp modified , text changed
Directorymetaprl/theories/base/base_auto_tactic.ml modified , text changed
Directorymetaprl/theories/base/base_auto_tactic.mli modified , text changed
Directorymetaprl/theories/base/base_cache.ml modified , text changed
Directorymetaprl/theories/base/base_dtactic.ml modified , text changed
Directorymetaprl/theories/base/base_rewrite.ml modified , text changed
Directorymetaprl/theories/base/typeinf.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_all.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_and.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_dall.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_dexists.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_empty.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_eq.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_eq_inner.ml modified , text changed
Directorymetaprl/theories/czf/czf_itt_exists.ml modified , text changed
[...]

  ViewVC Help
Powered by ViewVC 1.1.26