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 +---
 dev/core.dbg           |  1 -
 dev/doc/changes.md     | 10 ----------
 dev/ocamldebug-coq.run |  1 -
 dev/top_printers.ml    |  2 +-
 5 files changed, 2 insertions(+), 16 deletions(-)

(limited to 'dev')

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 *)
diff --git a/dev/core.dbg b/dev/core.dbg
index 18e82c352c..00a4355a48 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -17,5 +17,4 @@ load_printer vernac.cma
 load_printer stm.cma
 load_printer toplevel.cma
 load_printer intf.cma
-load_printer API.cma
 load_printer ltac_plugin.cmo
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index f6fbb69424..e616bd5663 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -12,16 +12,6 @@ All the bugs with a number below 1154 had to be renumbered, you can find
 a correspondence table [here](/dev/bugzilla2github_stripped.csv).
 All the other bugs kept their number.
 
-### Plugin API
-
-Coq 8.8 offers a new module overlay containing a proposed plugin API
-in `API/API.ml`; this overlay is enabled by adding the `-open API`
-flag to the OCaml compiler; this happens automatically for
-developments in the `plugin` folder and `coq_makefile`.
-
-However, `coq_makefile` can be instructed not to enable this flag by
-passing `-bypass-API`.
-
 ### ML API
 
 General deprecation
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index f4799f7b2c..3850c05fd9 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -23,7 +23,6 @@ exec $OCAMLDEBUG \
 	-I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
         -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
 	-I $COQTOP/toplevel -I $COQTOP/dev -I $COQTOP/config -I $COQTOP/ltac \
-        -I $COQTOP/API \
         -I $COQTOP/plugins/cc         -I $COQTOP/plugins/dp \
         -I $COQTOP/plugins/extraction -I $COQTOP/plugins/field \
         -I $COQTOP/plugins/firstorder -I $COQTOP/plugins/fourier \
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 832040ad2c..ff38257877 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -233,7 +233,7 @@ let ppenvwithcst e = pp
    str "[" ++ pr_rel_context e Evd.empty (rel_context e) ++ str "]" ++ spc() ++
    str "{" ++ Cmap_env.fold (fun a _ s -> Constant.print a ++ spc () ++ s) (Obj.magic e).Pre_env.env_globals.Pre_env.env_constants (mt ()) ++ str "}")
 
-let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (API.Global.env()) x))
+let pptac = (fun x -> pp(Ltac_plugin.Pptactic.pr_glob_tactic (Global.env()) x))
 
 let ppobj obj = Format.print_string (Libobject.object_tag obj)
 
-- 
cgit v1.2.3


From 2be81020d8533b7d275f820fad8f597929aa064e Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Tue, 26 Dec 2017 10:21:53 +0100
Subject: overlay for #6493

---
 dev/ci/user-overlays/06493-gares-API-remove-big-file.sh | 8 ++++++++
 1 file changed, 8 insertions(+)
 create mode 100644 dev/ci/user-overlays/06493-gares-API-remove-big-file.sh

(limited to 'dev')

diff --git a/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh
new file mode 100644
index 0000000000..9677b35253
--- /dev/null
+++ b/dev/ci/user-overlays/06493-gares-API-remove-big-file.sh
@@ -0,0 +1,8 @@
+if [ "$CI_PULL_REQUEST" = "6493" ] || [ "$CI_BRANCH" = "API/remove-big-file" ]; then
+    Equations_CI_BRANCH=API-removal
+    Equations_CI_GITURL=https://github.com/gares/Coq-Equations.git
+    coq_dpdgraph_CI_BRANCH=API-removal
+    coq_dpdgraph_CI_GITURL=https://github.com/gares/coq-dpdgraph.git
+    ltac2_CI_BRANCH=API-removal
+    ltac2_CI_GITURL=https://github.com/gares/ltac2.git
+fi
-- 
cgit v1.2.3