diff options
| -rw-r--r-- | parsing/pptactic.ml | 2 | ||||
| -rw-r--r-- | translate/ppconstrnew.ml | 24 | ||||
| -rw-r--r-- | translate/ppconstrnew.mli | 2 |
3 files changed, 27 insertions, 1 deletions
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index b09f0359c..4f6a47af5 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 7e71f5623..662649add 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 03084b8d2..44277a555 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 |