From b37d3f199e4521e2ae20cc96f0f2b04acc36c7cc Mon Sep 17 00:00:00 2001
From: Enrico Tassi
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.
---
 dev/base_include | 4 +---
 1 file changed, 1 insertion(+), 3 deletions(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 4dc9a0bee8..2a4ad4a157 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -18,12 +18,10 @@
 #directory "intf";;
 #directory "stm";;
 #directory "vernac";;
-#directory "../API";;
 
 #directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
 #directory "+camlp5";; (* Gramext is found in top_printers.ml *)
 
-#load "API.cma";;
 #use "top_printers.ml";;
 #use "vm_printers.ml";;
 
@@ -194,7 +192,7 @@ let qid = Libnames.qualid_of_string;;
 
 let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
 let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac_control;;
-let parse_tac    = API.Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
+let parse_tac    = Pcoq.parse_string Ltac_plugin.Pltac.tactic;;
 
 (* build a term of type glob_constr without type-checking or resolution of 
    implicit syntax *)
-- 
cgit v1.2.3