From 12965209478bd99dfbe57f07d5b525e51b903f22 Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 2 Aug 2002 17:17:42 +0000
Subject: Modules dans COQ\!\!\!\!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 dev/base_include | 12 +++++++++++-
 1 file changed, 11 insertions(+), 1 deletion(-)

(limited to 'dev/base_include')

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 *)
-- 
cgit v1.2.3