diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-21 20:04:58 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:39:25 +0200 |
| commit | 02d2f34e5c84f0169e884c07054a6fbfef9f365c (patch) | |
| tree | 5e55f22c5b20dcf694c00741a69dae6f1d993267 /printing/printer.ml | |
| parent | 95239fa33c5da60080833dabc3ced246680dfdf9 (diff) | |
Remove some unused values and types
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 35ddf2e8c..93d221f03 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) |