(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* HOL LIGHT pervasives                                                       *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2012-04-15                                                           *)
(* ========================================================================== *)


(*
This module contains things in HOL Light that clash and get overwriten.
This file needs to be loaded immediately after 
tactics.ml and lib.ml to get the intended values.
*)


(* from tactics *)

module Hol_pervasives = struct 

let e tac = refine(by(VALID tac));;

let r n = refine(rotate n);;

let g t =
  let fvs = sort (<) (map (fst o dest_var) (frees t)) in
  (if fvs <> [] then
     let errmsg = end_itlist (fun s t -> s^", "^t) fvs in
     warn true ("Free variables in goal: "^errmsg)
   else ());
   set_goal([],t);;

let b() =
  let l = !current_goalstack in
  if length l = 1 then failwith "Can't back up any more" else
  current_goalstack := tl l;
  !current_goalstack;;

let p() =
  !current_goalstack;;

(* HOL Light lib, in general raises Failure _ 
   unlike Ocaml List, which raises Not_found.  *)

let assoc = assoc;; 

let hd = hd;;

let tl = tl;;

let sort = sort;;

let prove = prove;;
let zip = zip;;

let find = find;;

let ISPECL = ISPECL;;


(* abs, sqrt, .... *)

end;;