[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...

2 files changed, 40 insertions, 0 deletions

diff --git a/engine/engine.mllib b/engine/engine.mllib
index a3614f6c4..a5df5a9fa 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/engine/evar_kinds.ml b/engine/evar_kinds.ml
new file mode 100644
index 000000000..c964ecf1f
--- /dev/null
+++ b/engine/evar_kinds.ml
@@ -0,0 +1,39 @@
+(************************************************************************)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
+(*   \VV/  **************************************************************)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
+(************************************************************************)
+
+open Names
+open Globnames
+open Misctypes
+
+(** The kinds of existential variable *)
+
+(** Should the obligation be defined (opaque or transparent (default)) or
+    defined transparent and expanded in the term? *)
+
+type obligation_definition_status = Define of bool | Expand
+
+type matching_var_kind = FirstOrderPatVar of patvar | SecondOrderPatVar of patvar
+
+type subevar_kind = Domain | Codomain | Body
+
+type t =
+  | ImplicitArg of global_reference * (int * Id.t option)
+     * bool (** Force inference *)
+  | BinderType of Name.t
+  | NamedHole of Id.t (* coming from some ?[id] syntax *)
+  | QuestionMark of obligation_definition_status * Name.t
+  | CasesType of bool (* true = a subterm of the type *)
+  | InternalHole
+  | TomatchTypeParameter of inductive * int
+  | GoalEvar
+  | ImpossibleCase
+  | MatchingVar of matching_var_kind
+  | VarInstance of Id.t
+  | SubEvar of subevar_kind option * Evar.t