diff options
Diffstat (limited to 'dev/base_include')
| -rw-r--r-- | dev/base_include | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index a9d8d78129..83d967ce44 100644 --- a/dev/base_include +++ b/dev/base_include @@ -6,10 +6,20 @@ #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;; @@ -38,7 +48,7 @@ let constr_of_string s = open Declarations;; let constbody_of_string s = - let b = Global.lookup_constant (path_of_string s) in + 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 *) |