diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /dev/base_include |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'dev/base_include')
-rw-r--r-- | dev/base_include | 76 |
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 + |