equal
deleted
inserted
replaced
208 |
208 |
209 |
209 |
210 (* init options *) |
210 (* init options *) |
211 |
211 |
212 fun init_options () = |
212 fun init_options () = |
213 (Future.ML_statistics := Options.default_bool "ML_statistics"; |
213 (ML_Pretty.print_depth (Options.default_int "ML_print_depth"); |
|
214 Future.ML_statistics := Options.default_bool "ML_statistics"; |
214 Multithreading.trace := Options.default_int "threads_trace"; |
215 Multithreading.trace := Options.default_int "threads_trace"; |
215 Multithreading.max_threads_update (Options.default_int "threads"); |
216 Multithreading.max_threads_update (Options.default_int "threads"); |
216 Goal.parallel_proofs := Options.default_int "parallel_proofs"); |
217 Goal.parallel_proofs := Options.default_int "parallel_proofs"); |
217 |
218 |
218 fun init_build_options () = |
219 fun init_build_options () = |