Remove some dead-code (thanks to ocaml warnings)

 The removed code isn't used locally and isn't exported in the signature

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