From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 printing/printer.ml | 5 -----
 1 file changed, 5 deletions(-)

(limited to 'printing/printer.ml')

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)
-- 
cgit v1.2.3