1 files changed, 76 insertions, 0 deletions
diff --git a/dev/base_include b/dev/base_include
new file mode 100644
index 00000000..17293776
--- /dev/null
+++ b/dev/base_include
@@ -0,0 +1,76 @@
+
+(* File to include to get some Coq facilities under the ocaml toplevel.
+   This file is loaded by include *)
+
+#cd".";;
+#directory "parsing";;
+#directory "interp";;
+#directory "toplevel";;
+#directory "library";;
+#directory "kernel";;
+#directory "pretyping";;
+#directory "lib";;
+#directory "proofs";;
+#directory "tactics";;
+#directory "translate";;
+#use "top_printers.ml";;
+
+#install_printer  (* identifier *) prid;;
+#install_printer  (* label *) prlab;;
+#install_printer prmsid;;
+#install_printer prmbid;;
+#install_printer prdir;;
+#install_printer prmp;;
+#install_printer  (* section_path *)  prsp;;
+#install_printer  (* qualid *)  prqualid;;
+#install_printer  (* kernel_name *) prkn;;
+#install_printer  (* constr *)  print_pure_constr;;
+
+(* parsing of names *)
+
+let qid = Libnames.qualid_of_string;;
+
+(* parsing of terms *)
+
+let parse_com   = Pcoq.parse_string Pcoq.Constr.constr;;
+let parse_tac = Pcoq.parse_string Pcoq.Tactic.tactic;;
+let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
+
+(* For compatibility reasons *)
+let parse_ast = parse_com;;
+
+(* build a term of type rawconstr without type-checking or resolution of 
+   implicit syntax *)
+
+let e s = Constrintern.interp_rawconstr Evd.empty (Global.env()) (parse_ast s);;
+
+(* For compatibility *)
+let raw_constr_of_string = e;;
+
+(* build a term of type constr with type-checking and resolution of 
+   implicit syntax *)
+
+let constr_of_string s = 
+  Constrintern.interp_constr Evd.empty (Global.env()) (parse_ast s);;
+
+(* get the body of a constant *)
+
+open Declarations;;
+
+let constbody_of_string s =
+  let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_sp (path_of_string s))) in
+  Util.out_some b.const_body;;
+
+(* Get the current goal *)
+
+let getgoal x = top_goal_of_pftreestate (Pfedit.get_pftreestate x);;
+
+let get_nth_goal n = nth_goal_of_pftreestate n (Pfedit.get_pftreestate ());;
+let current_goal () = get_nth_goal 1;;
+
+let pf_e gl s = 
+    Constrintern.interp_constr (project gl) (pf_env gl) (parse_ast s);;
+
+open Toplevel
+let go = loop
+