diff options
Diffstat (limited to 'parsing/prettyp.ml')
| -rw-r--r-- | parsing/prettyp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 538828fca2..9e6ff72d31 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -205,7 +205,7 @@ let pr_located_qualid = function | IndRef _ -> "Inductive" | ConstructRef _ -> "Constructor" | VarRef _ -> "Variable" in - str ref_str ++ spc () ++ pr_global ref + str ref_str ++ spc () ++ pr_path (Nametab.path_of_global ref) | Syntactic kn -> str "Notation" ++ spc () ++ pr_path (Nametab.path_of_syndef kn) | Dir dir -> |