diff options
| author | coq | 2002-08-02 17:17:42 +0000 |
|---|---|---|
| committer | coq | 2002-08-02 17:17:42 +0000 |
| commit | 12965209478bd99dfbe57f07d5b525e51b903f22 (patch) | |
| tree | 36a7f5e4802cd321caf02fed0be8349100be09fb /dev/base_include | |
| parent | 8b26fd6ba739d4f49fae99ed764b086022e44b50 (diff) | |
Modules dans COQ\!\!\!\!
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
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 *) |