diff options
| author | Gaetan Gilbert | 2017-04-21 20:04:58 +0200 |
|---|---|---|
| committer | Gaetan Gilbert | 2017-04-27 21:39:25 +0200 |
| commit | 02d2f34e5c84f0169e884c07054a6fbfef9f365c (patch) | |
| tree | 5e55f22c5b20dcf694c00741a69dae6f1d993267 /printing | |
| parent | 95239fa33c5da60080833dabc3ced246680dfdf9 (diff) | |
Remove some unused values and types
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/ppconstr.ml | 4 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 4 | ||||
| -rw-r--r-- | printing/printer.ml | 5 |
3 files changed, 0 insertions, 13 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 38eeda9b96..3041ac259e 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -212,10 +212,6 @@ let tag_var = tag Tag.variable | Some (_,ExplByName id) -> str "(" ++ pr_id id ++ str ":=" ++ pr ltop a ++ str ")" - let pr_opt_type pr = function - | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt () - | t -> cut () ++ str ":" ++ pr t - let pr_opt_type_spc pr = function | CHole (_,_,Misctypes.IntroAnonymous,_) -> mt () | t -> str " :" ++ pr_sep_com (fun()->brk(1,2)) (pr ltop) t diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index e4a87739b1..58475630e6 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -395,10 +395,6 @@ open Decl_kinds pr_opt (pr_guard_annot pr_lconstr_expr bl) guard ++ str":" ++ pr_spc_lconstr c) - let pr_priority = function - | None -> mt () - | Some i -> spc () ++ str "|" ++ spc () ++ int i - (**************************************) (* Pretty printer for vernac commands *) (**************************************) diff --git a/printing/printer.ml b/printing/printer.ml index 35ddf2e8cf..93d221f03f 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -370,11 +370,6 @@ let pr_context_limit_compact ?n env sigma = env ~init:(mt ()) in (sign_env ++ db_env) -(* compact printing an env (variables and de Bruijn). Separator: three - spaces between simple hyps, and newline otherwise *) -let pr_context_unlimited_compact env sigma = - pr_context_limit_compact env sigma - (* The number of printed hypothesis in a goal *) (* If [None], no limit *) let print_hyps_limit = ref (None : int option) |