-
Notifications
You must be signed in to change notification settings - Fork 1
/
init.ml
17 lines (14 loc) · 844 Bytes
/
init.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
(* ========================================================================= *)
(* Initialize theorem proving example code. *)
(* *)
(* Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.) *)
(* ========================================================================= *)
#load "nums.cma";; (* For Ocaml 3.06 *)
if let v = String.sub Sys.ocaml_version 0 4 in v >= "3.10"
then (Topdirs.dir_directory "+camlp5";
Topdirs.dir_load Format.std_formatter "camlp5o.cma")
else (Topdirs.dir_load Format.std_formatter "camlp4o.cma");;
type dummy_interactive = START_INTERACTIVE | END_INTERACTIVE;;
#use "initialization.ml";;
#use "Quotexpander.ml";;
#use "atp_interactive.ml";;