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

1 files changed, 96 insertions, 0 deletions

diff --git a/pretyping/locus.ml b/pretyping/locus.ml
new file mode 100644
index 000000000..95a2e495b
--- /dev/null
+++ b/pretyping/locus.ml
@@ -0,0 +1,96 @@
+(************************************************************************)
+(*         *   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 Misctypes
+
+(** Locus : positions in hypotheses and goals *)
+
+(** {6 Occurrences} *)
+
+type 'a occurrences_gen =
+  | AllOccurrences
+  | AllOccurrencesBut of 'a list (** non-empty *)
+  | NoOccurrences
+  | OnlyOccurrences of 'a list (** non-empty *)
+
+type occurrences_expr = (int or_var) occurrences_gen
+type 'a with_occurrences = occurrences_expr * 'a
+
+type occurrences = int occurrences_gen
+
+
+(** {6 Locations}
+
+  Selecting the occurrences in body (if any), in type, or in both *)
+
+type hyp_location_flag = InHyp | InHypTypeOnly | InHypValueOnly
+
+
+(** {6 Abstract clauses expressions}
+
+  A [clause_expr] (and its instance [clause]) denotes occurrences and
+  hypotheses in a goal in an abstract way; in particular, it can refer
+  to the set of all hypotheses independently of the effective contents
+  of the current goal
+
+  Concerning the field [onhyps]:
+   - [None] means *on every hypothesis*
+   - [Some l] means on hypothesis belonging to l *)
+
+type 'a hyp_location_expr = 'a with_occurrences * hyp_location_flag
+
+type 'id clause_expr =
+  { onhyps : 'id hyp_location_expr list option;
+    concl_occs : occurrences_expr }
+
+type clause = Id.t clause_expr
+
+
+(** {6 Concrete view of occurrence clauses} *)
+
+(** [clause_atom] refers either to an hypothesis location (i.e. an
+   hypothesis with occurrences and a position, in body if any, in type
+   or in both) or to some occurrences of the conclusion *)
+
+type clause_atom =
+  | OnHyp of Id.t * occurrences_expr * hyp_location_flag
+  | OnConcl of occurrences_expr
+
+(** A [concrete_clause] is an effective collection of occurrences
+    in the hypotheses and the conclusion *)
+
+type concrete_clause = clause_atom list
+
+
+(** {6 A weaker form of clause with no mention of occurrences} *)
+
+(** A [hyp_location] is an hypothesis together with a location *)
+
+type hyp_location = Id.t * hyp_location_flag
+
+(** A [goal_location] is either an hypothesis (together with a location)
+    or the conclusion (represented by None) *)
+
+type goal_location = hyp_location option
+
+
+(** {6 Simple clauses, without occurrences nor location} *)
+
+(** A [simple_clause] is a set of hypotheses, possibly extended with
+   the conclusion (conclusion is represented by None) *)
+
+type simple_clause = Id.t option list
+
+(** {6 A notion of occurrences allowing to express "all occurrences
+       convertible to the first which matches"} *)
+
+type 'a or_like_first = AtOccs of 'a | LikeFirst
+