diff options
| author | Pierre Letouzey | 2014-03-05 16:50:04 +0100 |
|---|---|---|
| committer | Pierre Letouzey | 2014-03-05 16:57:45 +0100 |
| commit | 8fc2509f354b02ec4e0a3eb6fabc329109686c47 (patch) | |
| tree | bf7f0738e36d861d57029985ea4f2d3e73d23c15 /printing | |
| parent | adfd437f8ae6aaf893119fa4730edecf067dede7 (diff) | |
Remove some dead-code (thanks to ocaml warnings)
The removed code isn't used locally and isn't exported in the signature
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/pptactic.ml | 5 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 10 | ||||
| -rw-r--r-- | printing/printer.ml | 5 |
3 files changed, 0 insertions, 20 deletions
diff --git a/printing/pptactic.ml b/printing/pptactic.ml index adb2ba0d08..520eac8abb 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -286,8 +286,6 @@ let pr_raw_alias prc prlc prtac prpat = pr_alias_gen (pr_raw_generic prc prlc prtac prpat pr_reference) let pr_glob_alias prc prlc prtac prpat = pr_alias_gen (pr_glb_generic prc prlc prtac prpat) -let pr_alias prc prlc prtac prpat = - pr_extend_gen (pr_top_generic prc prlc prtac prpat) (**********************************************************************) (* The tactic printer *) @@ -1025,9 +1023,6 @@ let pr_glob_tactic env = pr_glob_tactic_level env ltop (** Registering *) -let register_uniform_printer wit pr = - Genprint.register_print0 wit pr pr pr - let () = let pr_bool b = if b then str "true" else str "false" in let pr_unit _ = str "()" in diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 7bb1ceaa0d..430dfab4d8 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 diff --git a/printing/printer.ml b/printing/printer.ml index ad154ec554..0800374003 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -720,11 +720,6 @@ let pr_assumptionset env s = ] in prlist_with_sep fnl (fun x -> x) (Option.List.flatten assums) -open Typeclasses - -let pr_instance i = - pr_global (instance_impl i) - (** Inductive declarations *) open Termops |