Proofrecording/diffs/proofobjects_init.ml

   1 let (use_proofobjects, use_extended_proofobjects, use_coq) =
   2   try
   3     let n = Sys.getenv "HOLPROOFOBJECTS" in
   4     if n = "BASIC" then
   5       (true, false, false)
   6     else if n = "EXTENDED" then
   7       (true, true, false)
   8     else if n = "COQ" then
   9       (true, true, true)
  10     else
  11       (false, false, false)
  12   with Not_found -> (false, false, false);;
  13
  14 let _ =
  15   if use_proofobjects then
  16     if use_coq then
  17       loads "proofobjects_coq.ml"
  18     else
  19       loads "proofobjects_trt.ml"
  20   else
  21     loads "proofobjects_dummy.ml";;