diff options
| -rw-r--r-- | parsing/prettyp.ml | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index 4621f1bb27..1aa337373f 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -465,6 +465,10 @@ let print_name r = let kn = Nametab.locate_syntactic_definition qid in print_syntactic_def " = " kn with Not_found -> + try print_module true (Nametab.locate_module qid) + with Not_found -> + try print_modtype (Nametab.locate_modtype qid) + with Not_found -> user_err_loc (loc,"print_name",pr_qualid qid ++ spc () ++ str "not a defined object") |