From 02d2f34e5c84f0169e884c07054a6fbfef9f365c Mon Sep 17 00:00:00 2001
From: Gaetan Gilbert
Date: Fri, 21 Apr 2017 20:04:58 +0200
Subject: Remove some unused values and types

---
 tools/coqdoc/output.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'tools')

diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index 853bc29aa4..235f2588c8 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -64,7 +64,6 @@ val keyword : string -> loc -> unit
 val ident : string -> loc option -> unit
 val sublexer : char -> loc -> unit
 val sublexer_in_doc : char -> unit
-val initialize : unit -> unit
 
 val proofbox : unit -> unit
 
-- 
cgit v1.2.3