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 ++++
 dev/tools/Makefile.devel | 2 +-
 dev/top_printers.ml      | 2 ++
 dev/vm_printers.ml       | 1 +
 4 files changed, 8 insertions(+), 1 deletion(-)

(limited to 'dev')

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
diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel
index 8dcc70cf7f..ffdb1bdca9 100644
--- a/dev/tools/Makefile.devel
+++ b/dev/tools/Makefile.devel
@@ -5,7 +5,7 @@
 TOPDIR=.
 BASEDIR=
 
-SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel
+SOURCEDIRS=lib kernel library pretyping parsing proofs tactics toplevel API
 
 default:	usage noargument
 
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 07a47c8b7a..a1b3c81b9a 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -8,6 +8,7 @@
 
 (* Printers for the ocaml toplevel. *)
 
+open API
 open Util
 open Pp
 open Names
@@ -492,6 +493,7 @@ VERNAC COMMAND EXTEND PrintConstr
 END
 *)
 
+open Grammar_API
 open Genarg
 open Stdarg
 open Egramml
diff --git a/dev/vm_printers.ml b/dev/vm_printers.ml
index afa94a63e0..be6b914b6b 100644
--- a/dev/vm_printers.ml
+++ b/dev/vm_printers.ml
@@ -1,3 +1,4 @@
+open API
 open Format
 open Term
 open Names
-- 
cgit v1.2.3