diff options
Diffstat (limited to 'printing/ppvernac.ml')
| -rw-r--r-- | printing/ppvernac.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index f088477e7..e52239ba7 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -924,7 +924,8 @@ let rec pr_vernac = function | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr | VernacLocate loc -> let pr_locate =function - | LocateTerm qid -> pr_smart_global qid + | LocateAny qid -> pr_smart_global qid + | LocateTerm qid -> str "Term" ++ spc() ++ pr_smart_global qid | LocateFile f -> str"File" ++ spc() ++ qs f | LocateLibrary qid -> str"Library" ++ spc () ++ pr_module qid | LocateModule qid -> str"Module" ++ spc () ++ pr_module qid |