Modules dans COQ\!\!\!\!

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 11 deletions

diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index ad120fe19..fbee5ff27 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -16,33 +16,34 @@ open Pp
 open Nametab
 open Names
 open Nameops
+open Libnames
 open Coqast
 open Extend
 open Util
 
 let dfltpr ast = (str"#GENTERM " ++ print_ast ast);;
 
-let pr_global ref = pr_global_env (Global.env()) ref
+let pr_global ref = pr_global_env None ref
 
-let global_const_name sp =
-  try pr_global (ConstRef sp)
+let global_const_name kn =
+  try pr_global (ConstRef kn)
   with Not_found -> (* May happen in debug *)
-    (str ("CONST("^(string_of_path sp)^")"))
+    (str ("CONST("^(string_of_kn kn)^")"))
 
 let global_var_name id =
   try pr_global (VarRef id)
   with Not_found -> (* May happen in debug *)
     (str ("SECVAR("^(string_of_id id)^")"))
 
-let global_ind_name (sp,tyi) =
-  try pr_global (IndRef (sp,tyi))
+let global_ind_name (kn,tyi) =
+  try pr_global (IndRef (kn,tyi))
   with Not_found -> (* May happen in debug *)
-    (str ("IND("^(string_of_path sp)^","^(string_of_int tyi)^")"))
+    (str ("IND("^(string_of_kn kn)^","^(string_of_int tyi)^")"))
 
-let global_constr_name ((sp,tyi),i) =
-  try pr_global (ConstructRef ((sp,tyi),i))
+let global_constr_name ((kn,tyi),i) =
+  try pr_global (ConstructRef ((kn,tyi),i))
   with Not_found -> (* May happen in debug *)
-    (str ("CONSTRUCT("^(string_of_path sp)^","^(string_of_int tyi)
+    (str ("CONSTRUCT("^(string_of_kn kn)^","^(string_of_int tyi)
 		  ^","^(string_of_int i)^")"))
 
 let globpr gt = match gt with
@@ -89,7 +90,7 @@ let pr_constr = gentermpr
 
 let pr_pattern = gentermpr
 
-let pr_qualid qid = str (Nametab.string_of_qualid qid)
+let pr_qualid qid = str (string_of_qualid qid)
 
 open Rawterm