From 8893be32493e70c6ef81a6e206e137c94e85185a Mon Sep 17 00:00:00 2001
From: Jim Fehrle
Date: Mon, 21 May 2018 13:59:54 -0700
Subject: Remove the unused printer_pr mechanism.

---
 printing/printer.mli | 11 -----------
 1 file changed, 11 deletions(-)

(limited to 'printing/printer.mli')

diff --git a/printing/printer.mli b/printing/printer.mli
index 4af90e6a62..ac0e129792 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -222,14 +222,3 @@ val pr_assumptionset : env -> evar_map -> types ContextObjectMap.t -> Pp.t
 
 val pr_goal_by_id : proof:Proof.t -> Id.t -> Pp.t
 
-type printer_pr = {
- pr_subgoals            : ?pr_first:bool -> Pp.t option -> evar_map -> seeds:goal list -> shelf:goal list -> stack:int list -> unfocused:goal list -> goals:goal list -> Pp.t;
-
- pr_subgoal             : int -> evar_map -> goal list -> Pp.t;
- pr_goal                : goal sigma -> Pp.t;
-}
-
-val set_printer_pr : printer_pr -> unit
-
-val default_printer_pr : printer_pr
-
-- 
cgit v1.2.3