From 661940fd55a925a6f17f6025f5d15fc9f5647cf9 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Mon, 10 Oct 2016 10:59:22 +0200
Subject: Put all plugins behind an "API".

---
 dev/base_include | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 608624d06e..defea713d8 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -18,10 +18,12 @@
 #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";;
 
@@ -56,6 +58,8 @@
 
 (* Open main files *)
 
+open API
+open Grammar_API
 open Names
 open Term
 open Vars
-- 
cgit v1.2.3