[api] Relocate `intf` modules according to dependency-order.

In a component-based source code organization of Coq `intf` doesn't
fit very well, as it sits in bit of "limbo" between different
components, and indeed, encourages developers to place types in
sometimes random places wrt the hierarchy. For example, lower parts of
the system reference `Vernacexpr`, which morally lives in a pretty
higher part of the system.

We move all the files in `intf` to the lowest place their dependencies
can accommodate:

- `Misctypes`: is used by Declaremod, thus it has to go in `library`
  or below. Ideally, this file would disappear.
- `Evar_kinds`: it is used by files in `engine`, so that seems its
  proper placement.
- `Decl_kinds`: used in `library`, seems like the right place. [could
  also be merged.
- `Glob_term`: belongs to pretyping, where it is placed.
- `Locus`: ditto.
- `Pattern`: ditto.
- `Genredexpr`: depended by a few modules in `pretyping`, seems like
  the righ place.
- `Constrexpr`: used in `pretyping`, the use is a bit unfortunate and
  could be fixed, as this module should be declared in `interp` which
  is the one eliminating it.
- `Vernacexpr`: same problem than `Constrexpr`; this one can be fixed
  as it contains stuff it shouldn't. The right place should be `parsing`.
- `Extend`: Is placed in `pretyping` due to being used by `Vernacexpr`.
- `Notation_term`: First place used is `interp`, seems like the right place.

Additionally, for some files it could be worth to merge files of the
form `Foo` with `Foo_ops` in the medium term, as to create proper ADT
modules as done in the kernel with `Name`, etc...

25 files changed, 16 insertions, 44 deletions

diff --git a/.github/CODEOWNERS b/.github/CODEOWNERS
index 029b55b9ad..7f3ee5c37d 100644
--- a/.github/CODEOWNERS
+++ b/.github/CODEOWNERS
@@ -86,11 +86,6 @@
 /interp/          @herbelin
 # Secondary maintainer @ejgallego
 
-########## Interfaces ##########
-
-/intf/            @letouzey
-# Secondary maintainer @ppedrot
-
 ########## Kernel ##########
 
 /kernel/          @maximedenes
diff --git a/.merlin b/.merlin
index d60f5037bb..40db609509 100644
--- a/.merlin
+++ b/.merlin
@@ -10,8 +10,6 @@ S kernel
 B kernel
 S kernel/byterun
 B kernel/byterun
-S intf
-B intf
 S library
 B library
 S engine
diff --git a/META.coq b/META.coq
index 30bfdd67a7..3414ccbd40 100644
--- a/META.coq
+++ b/META.coq
@@ -90,19 +90,6 @@ package "library" (
 
 )
 
-package "intf" (
-
-  description = "Coq Public Data Types"
-  version     = "8.8"
-
-  requires    = "coq.library"
-
-  directory   = "intf"
-
-  archive(byte)    = "intf.cma"
-  archive(native)  = "intf.cmxa"
-)
-
 package "engine" (
 
   description = "Coq Tactic Engine"
diff --git a/Makefile.common b/Makefile.common
index 9a30e2a4ce..eed41fbe71 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -75,7 +75,7 @@ INSTALLSH:=./install.sh
 MKDIR:=install -d
 
 CORESRCDIRS:=\
-  config 	clib 		lib		kernel	intf	kernel/byterun	library \
+  config 	clib 		lib		kernel		kernel/byterun	library \
   engine 	pretyping	interp	proofs	parsing 	printing \
   tactics 	vernac		stm		toplevel
 
@@ -102,7 +102,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \
 # respecting this order is useful for developers that want to load or link
 # the libraries directly
 
-CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/library.cma \
+CORECMA:=clib/clib.cma lib/lib.cma kernel/kernel.cma library/library.cma \
         engine/engine.cma pretyping/pretyping.cma interp/interp.cma proofs/proofs.cma \
         parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \
 	stm/stm.cma toplevel/toplevel.cma
diff --git a/configure.ml b/configure.ml
index 6c052b63b6..2ac705ad27 100644
--- a/configure.ml
+++ b/configure.ml
@@ -1212,7 +1212,7 @@ let write_configml f =
 
   let core_src_dirs = [ "config"; "dev"; "lib"; "clib"; "kernel"; "library";
                         "engine"; "pretyping"; "interp"; "parsing"; "proofs";
-                        "tactics"; "toplevel"; "printing"; "intf";
+                        "tactics"; "toplevel"; "printing";
                         "grammar"; "ide"; "stm"; "vernac" ] in
   let core_src_dirs = List.fold_left (fun acc core_src_subdir -> acc ^ "  \"" ^ core_src_subdir ^ "\";\n")
                                     ""
diff --git a/dev/base_include b/dev/base_include
index e76044f415..2f7183dd63 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -15,7 +15,6 @@
 #directory "tactics";;
 #directory "printing";;
 #directory "grammar";;
-#directory "intf";;
 #directory "stm";;
 #directory "vernac";;
 
diff --git a/dev/core.dbg b/dev/core.dbg
index 57c136900d..edf67020ab 100644
--- a/dev/core.dbg
+++ b/dev/core.dbg
@@ -16,5 +16,4 @@ load_printer tactics.cma
 load_printer vernac.cma
 load_printer stm.cma
 load_printer toplevel.cma
-load_printer intf.cma
 load_printer ltac_plugin.cmo
diff --git a/dev/doc/coq-src-description.txt b/dev/doc/coq-src-description.txt
index b3d49b7e56..764d482957 100644
--- a/dev/doc/coq-src-description.txt
+++ b/dev/doc/coq-src-description.txt
@@ -17,12 +17,6 @@ toplevel
 Special components
 ------------------
 
-intf :
-
- Contains mli-only interfaces, many of them providing a.s.t.
- used for dialog bewteen coq components. Ex: Constrexpr.constr_expr
- produced by parsing and transformed by interp.
-
 grammar :
 
  Camlp5 syntax extensions. The file grammar/grammar.cma is used
diff --git a/dev/ocamldebug-coq.run b/dev/ocamldebug-coq.run
index f3e60edea8..8f1c165dd4 100644
--- a/dev/ocamldebug-coq.run
+++ b/dev/ocamldebug-coq.run
@@ -18,7 +18,7 @@ exec $OCAMLDEBUG \
 	-I $CAMLP5LIB -I +threads \
 	-I $COQTOP \
 	-I $COQTOP/config -I $COQTOP/printing -I $COQTOP/grammar -I $COQTOP/clib \
-	-I $COQTOP/lib -I $COQTOP/intf -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
+	-I $COQTOP/lib -I $COQTOP/kernel -I $COQTOP/kernel/byterun \
 	-I $COQTOP/library -I $COQTOP/engine \
 	-I $COQTOP/pretyping -I $COQTOP/parsing -I $COQTOP/vernac \
         -I $COQTOP/interp -I $COQTOP/proofs -I $COQTOP/tactics -I $COQTOP/stm \
diff --git a/engine/engine.mllib b/engine/engine.mllib
index a3614f6c4a..a5df5a9fa0 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -2,6 +2,7 @@ Universes
 Univops
 UState
 Nameops
+Evar_kinds
 Evd
 EConstr
 Namegen
diff --git a/intf/evar_kinds.ml b/engine/evar_kinds.ml
index c964ecf1f5..c964ecf1f5 100644
--- a/intf/evar_kinds.ml
+++ b/engine/evar_kinds.ml
diff --git a/interp/interp.mllib b/interp/interp.mllib
index bb22cf468d..61313acc48 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -1,6 +1,7 @@
 Tactypes
 Stdarg
 Genintern
+Notation_term
 Notation_ops
 Notation
 Syntax_def
diff --git a/intf/notation_term.ml b/interp/notation_term.ml
index a9c2e2a532..a9c2e2a532 100644
--- a/intf/notation_term.ml
+++ b/interp/notation_term.ml
diff --git a/intf/intf.mllib b/intf/intf.mllib
deleted file mode 100644
index 2b8960d3f2..0000000000
--- a/intf/intf.mllib
+++ /dev/null
@@ -1,11 +0,0 @@
-Constrexpr
-Evar_kinds
-Genredexpr
-Locus
-Extend
-Notation_term
-Decl_kinds
-Glob_term
-Misctypes
-Pattern
-Vernacexpr
diff --git a/intf/decl_kinds.ml b/library/decl_kinds.ml
index 0d32853116..0d32853116 100644
--- a/intf/decl_kinds.ml
+++ b/library/decl_kinds.ml
diff --git a/library/library.mllib b/library/library.mllib
index e43bfb5a1f..1c03688470 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -4,7 +4,9 @@ Libobject
 Summary
 Nametab
 Global
+Decl_kinds
 Lib
+Misctypes
 Declaremods
 Loadpath
 Library
diff --git a/intf/misctypes.ml b/library/misctypes.ml
index 72db3b31cb..72db3b31cb 100644
--- a/intf/misctypes.ml
+++ b/library/misctypes.ml
diff --git a/intf/constrexpr.ml b/pretyping/constrexpr.ml
index fda31756a9..fda31756a9 100644
--- a/intf/constrexpr.ml
+++ b/pretyping/constrexpr.ml
diff --git a/intf/extend.ml b/pretyping/extend.ml
index 734b859f60..734b859f60 100644
--- a/intf/extend.ml
+++ b/pretyping/extend.ml
diff --git a/intf/genredexpr.ml b/pretyping/genredexpr.ml
index 80697461a6..80697461a6 100644
--- a/intf/genredexpr.ml
+++ b/pretyping/genredexpr.ml
diff --git a/intf/glob_term.ml b/pretyping/glob_term.ml
index 84be15552a..84be15552a 100644
--- a/intf/glob_term.ml
+++ b/pretyping/glob_term.ml
diff --git a/intf/locus.ml b/pretyping/locus.ml
index 95a2e495be..95a2e495be 100644
--- a/intf/locus.ml
+++ b/pretyping/locus.ml
diff --git a/intf/pattern.ml b/pretyping/pattern.ml
index 76367b612a..76367b612a 100644
--- a/intf/pattern.ml
+++ b/pretyping/pattern.ml
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index ae4ad0be7d..d98026bc60 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -1,5 +1,5 @@
 Geninterp
-Ltac_pretype
+Locus
 Locusops
 Pretype_errors
 Reductionops
@@ -16,12 +16,19 @@ Evarsolve
 Recordops
 Evarconv
 Typing
+Constrexpr
+Genredexpr
 Miscops
+Glob_term
+Ltac_pretype
 Glob_ops
 Redops
+Pattern
 Patternops
 Constr_matching
 Tacred
+Extend
+Vernacexpr
 Typeclasses_errors
 Typeclasses
 Classops
diff --git a/intf/vernacexpr.ml b/pretyping/vernacexpr.ml
index 4e1c986f16..4e1c986f16 100644
--- a/intf/vernacexpr.ml
+++ b/pretyping/vernacexpr.ml