Merge PR #6493: [API] remove large file containing duplicate interfaces

6 files changed, 10 insertions, 16 deletions

diff --git a/dev/base_include b/dev/base_include
index 4dc9a0bee..2a4ad4a15 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/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 000000000..9677b3525
--- /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
diff --git a/dev/core.dbg b/dev/core.dbg
index 18e82c352..00a4355a4 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 f6fbb6942..e616bd566 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 f4799f7b2..3850c05fd 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 832040ad2..ff3825787 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)