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


From 11723417c3c3c76b121f5548948268961b621a49 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Wed, 7 Jun 2017 08:39:26 +0200
Subject: add overlays

---
 dev/ci/ci-user-overlay.sh | 13 +++++++++++++
 1 file changed, 13 insertions(+)

(limited to 'dev')

diff --git a/dev/ci/ci-user-overlay.sh b/dev/ci/ci-user-overlay.sh
index 195ede6d00..d1a2af4174 100644
--- a/dev/ci/ci-user-overlay.sh
+++ b/dev/ci/ci-user-overlay.sh
@@ -30,3 +30,16 @@ if [ $TRAVIS_PULL_REQUEST == "669" ] || [ $TRAVIS_BRANCH == "ssr-merge" ]; then
     mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
 fi
 
+echo "DEBUG: ci-user-overlay.sh 0"
+if [ $TRAVIS_PULL_REQUEST = "652" ] || [ $TRAVIS_BRANCH == "trunk__API" ]; then
+    echo "DEBUG: ci-user-overlay.sh 1"
+    echo
+    #mathcomp_CI_BRANCH=remove-sigma
+    #mathcomp_CI_GITURL=https://github.com/maximedenes/math-comp.git
+    fiat_parsers_CI_BRANCH=remove-sigma
+    fiat_parsers_CI_GITURL=https://github.com/maximedenes/fiat.git
+    bedrock_src_CI_BRANCH=remove-sigma
+    bedrock_src_CI_GITURL=https://github.com/maximedenes/bedrock.git
+    bedrock_facade_CI_BRANCH=remove-sigma
+    bedrock_facade_CI_GITURL=https://github.com/maximedenes/bedrock.git
+fi
-- 
cgit v1.2.3