diff options
Diffstat (limited to 'printing/ppvernac.ml')
-rw-r--r-- | printing/ppvernac.ml | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 7bb1ceaa0..430dfab4d 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -130,17 +130,7 @@ let pr_search a b pr_p = match a with | SearchRewrite c -> str"SearchRewrite" ++ spc() ++ pr_p c ++ pr_in_out_modules b | SearchAbout sl -> str"Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b -let pr_locality_full = function - | None -> mt () - | Some true -> str "Local" ++ spc () - | Some false -> str "Global "++ spc () - let pr_locality local = if local then str "Local" ++ spc () else mt () -let pr_non_locality local = if local then mt () else str "Global" ++ spc () -let pr_section_locality local = - if Lib.sections_are_opened () && not local then str "Global " - else if not (Lib.sections_are_opened ()) && local then str "Local " - else mt () let pr_explanation (e,b,f) = let a = match e with |