Merge PR#652: Put all plugins behind an "API".

5 files changed, 21 insertions, 1 deletions

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/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
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