From b37d3f199e4521e2ae20cc96f0f2b04acc36c7cc Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Fri, 22 Dec 2017 14:11:55 +0100
Subject: [API] remove large file containing duplicate interfaces

... in favor of having Public/Internal sub modules in each and
every module grouping functions according to their intended client.
---
 Makefile.doc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.doc')

diff --git a/Makefile.doc b/Makefile.doc
index 1b0803f19..8cb9c9f0f 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -387,7 +387,7 @@ OCAMLDOCDIR=dev/ocamldoc
 
 DOCMLIS=$(wildcard ./lib/*.mli ./intf/*.mli ./kernel/*.mli ./library/*.mli \
 	./engine/*.mli ./pretyping/*.mli ./interp/*.mli printing/*.mli \
-	./parsing/*.mli ./proofs/*.mli API/API.mli \
+	./parsing/*.mli ./proofs/*.mli \
 	./tactics/*.mli ./stm/*.mli ./toplevel/*.mli ./ltac/*.mli)
 
 # Defining options to generate dependencies graphs
-- 
cgit v1.2.3