Ajout pr_global_reference et is_visible

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

2 files changed, 17 insertions, 1 deletions

diff --git a/parsing/printer.ml b/parsing/printer.ml
index 3bda750b0b..ff4713f794 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -26,8 +26,16 @@ let pr_global k oper =
   [< 'sTR (string_of_id id) >]
 *)
 
+let is_visible sp id =
+  match Nametab.sp_of_id CCI id with
+    | VarRef sp' -> sp' = sp
+    | ConstRef sp' -> sp' = sp
+    | IndRef (sp',_) -> dirpath sp' = dirpath sp
+    | ConstructRef ((sp',_),_) -> dirpath sp' = dirpath sp
+    | EvarRef _ -> anomaly "is_visible: should not occur"
+  
 let pr_qualified_path sp id =
-  if Nametab.sp_of_id (kind_of_path sp) id = sp then [<'sTR(string_of_id id)>]
+  if is_visible sp id then [<'sTR(string_of_id id)>]
   else [<'sTR(string_of_path (make_path (dirpath sp) id (kind_of_path sp)))>]
 
 let global_const_name sp =
@@ -117,12 +125,16 @@ let pr_inductive env ind = gentermpr (ast_of_inductive env ind)
 let pr_constructor env cstr =
   gentermpr (ast_of_constructor env cstr)
 
+let pr_global_reference env ref =
+  gentermpr (ast_of_ref (ast_of_constr false env) ref)
+
 open Pattern
 let pr_ref_label = function (* On triche sur le contexte *)
   | ConstNode sp -> pr_constant (Global.env()) (sp,[||])
   | IndNode sp -> pr_inductive (Global.env()) (sp,[||])
   | CstrNode sp -> pr_constructor (Global.env()) (sp,[||])
   | VarNode id -> print_id id
+  | SectionVarNode sp -> print_id (basename sp)
 
 let pr_cases_pattern t = gentermpr (Termast.ast_of_cases_pattern t)
 let pr_rawterm t = gentermpr (Termast.ast_of_rawconstr t)
diff --git a/parsing/printer.mli b/parsing/printer.mli
index d9d3b5ce5f..1c53def26d 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -30,6 +30,7 @@ val pr_constant     : env -> constant -> std_ppcmds
 val pr_existential  : env -> existential -> std_ppcmds
 val pr_constructor  : env -> constructor -> std_ppcmds
 val pr_inductive    : env -> inductive -> std_ppcmds
+val pr_global_reference : env -> global_reference -> std_ppcmds
 val pr_ref_label    : constr_label -> std_ppcmds
 val pr_pattern      : constr_pattern -> std_ppcmds
 val pr_pattern_env  : names_context -> constr_pattern -> std_ppcmds
@@ -51,6 +52,9 @@ val fprterm         : constr -> std_ppcmds
 val fprtype_env     : env -> types -> std_ppcmds
 val fprtype         : types -> std_ppcmds
 
+val is_visible      : section_path -> identifier -> bool
+
 (* For compatibility *)
 val fterm0          : env -> constr -> std_ppcmds
 (*i*)
+