let flyspeck_dir = "/mnt/Repository/text_formalization";;
let hollight_dir = "";;

load_path := flyspeck_dir :: !load_path;;

let flyspeck_needs = needs;;

map needs [
	"Multivariate/flyspeck.ml";
	"Rqe/num_calc_simp.ml";
	"general/sphere.hl";
	"general/prove_by_refinement.hl";
];;

#load "unix.cma";;
let process_to_string unixstring =
  let p = Unix.open_process_in unixstring
  and b = Buffer.create 64 in
  let rec read () = Buffer.add_channel b p 1; read () in
    try read () with End_of_file -> (Unix.close_process_in p; Buffer.contents b);;


open Prove_by_refinement;;

map needs [
	"general/flyspeck_lib.hl";
	"leg/collect_geom2.hl";
	"leg/enclosed_def.hl";
	"trigonometry/trig2.hl";
];;

map needs [
	"jordan/lib_ext.hl";
	"jordan/refinement.hl";
	"jordan/parse_ext_override_interface.hl";
	"jordan/real_ext.hl";
	"jordan/hash_term.hl";
];;


prioritize_real();;
map needs [
	"jordan/tactics_jordan.hl";
	"jordan/num_ext_nabs.hl";
	"jordan/taylor_atn.hl";
	"jordan/float.hl";
	"jordan/flyspeck_constants.hl";
];;

map needs [
	"nonlinear/ineq.hl";
	"nonlinear/lemma.hl";
];;