Deplacement de Ppvernacnew.pr_reference dans Ppconstrnew pour utilisation par Pptactic

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

3 files changed, 27 insertions, 1 deletions

diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index b09f0359c7..4f6a47af52 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -676,7 +676,7 @@ and prtac x = pr6 x
 in (prtac,pr0,pr_match_rule false pr_pat pr_tac)
 
 let pr_raw_extend prc prlc prtac = 
-  pr_extend_gen (pr_raw_generic prc prlc prtac pr_reference)
+  pr_extend_gen (pr_raw_generic prc prlc prtac Ppconstrnew.pr_reference)
 let pr_glob_extend prc prlc prtac =
   pr_extend_gen (pr_glob_generic prc prlc prtac)
 let pr_extend prc prlc prtac =
diff --git a/translate/ppconstrnew.ml b/translate/ppconstrnew.ml
index 7e71f56239..662649add1 100644
--- a/translate/ppconstrnew.ml
+++ b/translate/ppconstrnew.ml
@@ -665,6 +665,30 @@ let pr_rawconstr_env_no_translate env c =
 let pr_lrawconstr_env_no_translate env c =
   pr ltop (Constrextern.extern_rawconstr (Termops.vars_of_env env) c)
 
+(* Printing reference with translation *)
+
+let pr_reference r =
+  let loc = loc_of_reference r in
+  try match Nametab.extended_locate (snd (qualid_of_reference r)) with
+    | TrueGlobal ref ->
+        pr_with_comments loc
+	  (pr_reference (Constrextern.extern_reference loc Idset.empty ref))
+    | SyntacticDef kn ->
+	let is_coq_root d =
+	  let d = repr_dirpath d in
+	  d <> [] & string_of_id (list_last d) = "Coq" in
+        let dir,id = repr_path (sp_of_syntactic_definition kn) in
+	let r =
+          if (is_coq_root (Lib.library_dp()) or is_coq_root dir) then
+	    (match Syntax_def.search_syntactic_definition loc kn with
+	      | RRef (_,ref) ->
+		  Constrextern.extern_reference dummy_loc Idset.empty ref
+              | _ -> r)
+          else r
+	in pr_with_comments loc (pr_reference r)
+  with Not_found ->
+    error_global_not_found (snd (qualid_of_reference r))
+
 (** constr printers *)
 
 let pr_term_env env  c = pr lsimple (Constrextern.extern_constr false env c)
diff --git a/translate/ppconstrnew.mli b/translate/ppconstrnew.mli
index 03084b8d25..44277a5552 100644
--- a/translate/ppconstrnew.mli
+++ b/translate/ppconstrnew.mli
@@ -71,6 +71,8 @@ val pr_lrawconstr_env : env -> rawconstr -> std_ppcmds
 val pr_rawconstr_env_no_translate : env -> rawconstr -> std_ppcmds
 val pr_lrawconstr_env_no_translate : env -> rawconstr -> std_ppcmds
 
+val pr_reference : reference -> std_ppcmds
+
 (** constr printers *)
 
 val pr_term_env : env -> constr -> std_ppcmds