diff options
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/dev/base_include b/dev/base_include index 83d967ce4..cadbc5cf1 100644 --- a/dev/base_include +++ b/dev/base_include @@ -3,6 +3,15 @@ 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";; #use "top_printers.ml";; #install_printer (* identifier *) prid;; @@ -32,7 +41,7 @@ let parse_ast = parse_com;; (* build a term of type rawconstr without type-checking or resolution of implicit syntax *) -let e s = Astterm.interp_rawconstr Evd.empty (Global.env()) (parse_ast s);; +let e s = Constrintern.interp_rawconstr Evd.empty (Global.env()) (parse_ast s);; (* For compatibility *) let raw_constr_of_string = e;; @@ -41,7 +50,7 @@ let raw_constr_of_string = e;; implicit syntax *) let constr_of_string s = - Astterm.interp_constr Evd.empty (Global.env()) (parse_ast s);; + Constrintern.interp_constr Evd.empty (Global.env()) (parse_ast s);; (* get the body of a constant *) @@ -59,7 +68,7 @@ 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 = - Astterm.interp_constr (project gl) (pf_env gl) (parse_ast s);; + Constrintern.interp_constr (project gl) (pf_env gl) (parse_ast s);; open Toplevel let go = loop |