9 files changed, 54 insertions, 33 deletions
diff --git a/dev/README b/dev/README
index b446c3e974..6b83579def 100644
--- a/dev/README
+++ b/dev/README
@@ -1,4 +1,4 @@
-This directory contains informations and tools to help developing the
+This directory contains information and tools to help develop the
                              Coq system
                        ======================
 
@@ -6,30 +6,30 @@ This directory contains informations and tools to help developing the
 Debugging and profiling (in current directory - see doc/debugging.txt)
 -----------------------
 
-ocamldebug-coq: to launch ocaml debugger
+ocamldebug-coq: to launch ocaml debugger (generated by the configure script)
 
-db:      to install pretty-printers from ocaml debugger
-base_db: to install raw pretty-printers from ocaml debugger
+db:           to install pretty-printers from ocaml debugger
+base_db:      to install raw pretty-printers from ocaml debugger
 
-include:      to install pretty-printers from ocaml toplevel
+include:      to install pretty-printers from ocaml toplevel (use with the coq Drop command)
 base_include: to install raw pretty-printers from ocaml toplevel
 
-vm_printers.ml, dev_printers.ml: ML pretty-printers for debugging
+vm_printers.ml, top_printers.ml: ML pretty-printers for debugging
 
 
-Miscellaneous informations about the code (directory doc)
+Miscellaneous information about the code (directory doc)
 -----------------------------------------
 
-changes.txt:   (partial) per-version summary of the evolutions of Coq ML source
-style.txt:     a few style recommendations for writing Coq ML files
-debugging.txt: help for debugging or profiling
-universes.txt: help to debug universes
-translate.txt: help to use coq translator
+changes.md:     (partial) per-version summary of the evolution of Coq ML source
+style.txt:      a few style recommendations for writing Coq ML files
+debugging.md:   help for debugging or profiling
+universes.txt:  help for debugging universes
+translate.txt:  help for using coq translator
 extensions.txt: some help about TACTIC EXTEND
 
-header:        standard header for Coq ML files
-perf-analysis: analysis of perfs measured on the compilation of user contribs
-cic.dtd:       official dtd of the calc. of ind. constr. for im/ex-portation
+header:         standard header for Coq ML files
+perf-analysis:  analysis of perfs measured on the compilation of user contribs
+cic.dtd:        official dtd of the calc. of ind. constr. for im/ex-portation
 
 
 Documentation of ML interfaces using ocamldoc (directory ocamldoc/html)
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/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh
new file mode 100644
index 0000000000..c2e3670380
--- /dev/null
+++ b/dev/ci/user-overlays/06405-maximedenes-rm-local-polymorphic-flag.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "6405" ] || [ "$CI_BRANCH" = "rm-local-polymorphic-flag" ]; then
+    Equations_CI_BRANCH=rm-local-polymorphic-flag
+    Equations_CI_GITURL=https://github.com/maximedenes/Coq-Equations
+fi
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
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/doc/debugging.md b/dev/doc/debugging.md
index fa145d498a..fd3cbd1bc3 100644
--- a/dev/doc/debugging.md
+++ b/dev/doc/debugging.md
@@ -22,8 +22,8 @@ Debugging from Coq toplevel using Caml trace mechanism
   printers too.
 
 
-Debugging from Caml debugger
-============================
+Debugging with ocamldebug from Emacs
+====================================
 
    Requires [Tuareg mode](https://github.com/ocaml/tuareg) in Emacs.\
    Coq must be configured with `-local` (`./configure -local`) and the
@@ -59,6 +59,29 @@ Debugging from Caml debugger
      from the debugger. If this happens, unset the variable, re-start Emacs, and 
      run the debugger again.
 
+Debugging with ocamldebug from the command line
+===============================================
+
+In the `coq` directory:
+1. (on Cygwin/Windows) Pass the `-no-custom` option to the `configure` script before building Coq.
+2. Run `make` (to compile the .v files)
+3. Run `make byte`
+4. (on Cygwin/Windows) Add the full pathname of the directory `.../kernel/byterun` to your bash PATH.
+   Alternatively, copy the file `kernel/byterun/dllcoqrun.dll` to a directory that is in the PATH.  (The
+   CAML_LD_LIBRARY_PATH mechanism described at the end of INSTALL isn't working.)
+5. Run `dev/ocamldebug-coq bin/coqtop.byte`  (on Cygwin/Windows, use `... bin/coqtop.byte.exe`)
+6. Enter `source db` to load printers
+7. Enter `set arguments -coqlib .` so Coq can find plugins, theories, etc.
+8. See the ocamldebug manual for more information.  A few points:
+   - use `break @ Printer 501` to set a breakpoint on line 501 in the Printer module (printer.ml).
+     `break` can be abbreviated as `b`.
+   - `backtrace` or `bt` to see the call stack
+   - `step` or `s` goes into called functions; `next` or `n` skips over them
+   - `list` or `li` shows the code just before and after the current stack frame
+   - `print <var>` or `p <var>` to see the value of a variable
+Note that `make byte` doesn't recompile .v files.  `make` recompiles all of them if there
+are changes in any .ml file--safer but much slower.
+
 Global gprof-based profiling
 ============================
 
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)