[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, 125 insertions, 0 deletions

diff --git a/interp/interp.mllib b/interp/interp.mllib
index bb22cf468..61313acc4 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/interp/notation_term.ml b/interp/notation_term.ml
new file mode 100644
index 000000000..a9c2e2a53
--- /dev/null
+++ b/interp/notation_term.ml
@@ -0,0 +1,124 @@
+(************************************************************************)
+(*         *   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
+open Glob_term
+
+(** [notation_constr] *)
+
+(** [notation_constr] is the subtype of [glob_constr] allowed in syntactic
+    extensions (i.e. notations).
+    No location since intended to be substituted at any place of a text.
+    Complex expressions such as fixpoints and cofixpoints are excluded,
+    as well as non global expressions such as existential variables. *)
+
+type notation_constr =
+  (** Part common to [glob_constr] and [cases_pattern] *)
+  | NRef of global_reference
+  | NVar of Id.t
+  | NApp of notation_constr * notation_constr list
+  | NHole of Evar_kinds.t * Misctypes.intro_pattern_naming_expr * Genarg.glob_generic_argument option
+  | NList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
+  (** Part only in [glob_constr] *)
+  | NLambda of Name.t * notation_constr * notation_constr
+  | NProd of Name.t * notation_constr * notation_constr
+  | NBinderList of Id.t * Id.t * notation_constr * notation_constr * (* associativity: *) bool
+  | NLetIn of Name.t * notation_constr * notation_constr option * notation_constr
+  | NCases of Constr.case_style * notation_constr option *
+      (notation_constr * (Name.t * (inductive * Name.t list) option)) list *
+      (cases_pattern list * notation_constr) list
+  | NLetTuple of Name.t list * (Name.t * notation_constr option) *
+      notation_constr * notation_constr
+  | NIf of notation_constr * (Name.t * notation_constr option) *
+      notation_constr * notation_constr
+  | NRec of fix_kind * Id.t array *
+      (Name.t * notation_constr option * notation_constr) list array *
+      notation_constr array * notation_constr array
+  | NSort of glob_sort
+  | NCast of notation_constr * notation_constr cast_type
+  | NProj of Projection.t * notation_constr
+
+(** Note concerning NList: first constr is iterator, second is terminator;
+    first id is where each argument of the list has to be substituted
+    in iterator and snd id is alternative name just for printing;
+    boolean is associativity *)
+
+(** Types concerning notations *)
+
+type scope_name = string
+
+type tmp_scope_name = scope_name
+
+type subscopes = tmp_scope_name option * scope_name list
+
+(** Type of the meta-variables of an notation_constr: in a recursive pattern x..y,
+    x carries the sequence of objects bound to the list x..y  *)
+
+type notation_binder_source =
+  (* This accepts only pattern *)
+  (* NtnParsedAsPattern true means only strict pattern (no single variable) at printing *)
+  | NtnParsedAsPattern of bool
+  (* This accepts only ident *)
+  | NtnParsedAsIdent
+  (* This accepts ident, or pattern, or both *)
+  | NtnBinderParsedAsConstr of Extend.constr_as_binder_kind
+
+type notation_var_instance_type =
+  | NtnTypeConstr | NtnTypeBinder of notation_binder_source | NtnTypeConstrList | NtnTypeBinderList
+
+(** Type of variables when interpreting a constr_expr as a notation_constr:
+    in a recursive pattern x..y, both x and y carry the individual type
+    of each element of the list x..y *)
+type notation_var_internalization_type =
+  | NtnInternTypeAny | NtnInternTypeOnlyBinder
+
+(** This characterizes to what a notation is interpreted to *)
+type interpretation =
+    (Id.t * (subscopes * notation_var_instance_type)) list *
+    notation_constr
+
+type reversibility_status = APrioriReversible | HasLtac | NonInjective of Id.t list
+
+type notation_interp_env = {
+  ninterp_var_type : notation_var_internalization_type Id.Map.t;
+  ninterp_rec_vars : Id.t Id.Map.t;
+}
+
+type grammar_constr_prod_item =
+  | GramConstrTerminal of Tok.t
+  | GramConstrNonTerminal of Extend.constr_prod_entry_key * Id.t option
+  | GramConstrListMark of int * bool * int
+    (* tells action rule to make a list of the n previous parsed items;
+       concat with last parsed list when true; additionally release
+       the p last items as if they were parsed autonomously *)
+
+(** Dealing with precedences *)
+
+type precedence = int
+type parenRelation = L | E | Any | Prec of precedence
+type tolerability = precedence * parenRelation
+
+type level = precedence * tolerability list * Extend.constr_entry_key list
+
+(** Grammar rules for a notation *)
+
+type one_notation_grammar = {
+  notgram_level : level;
+  notgram_assoc : Extend.gram_assoc option;
+  notgram_notation : Constrexpr.notation;
+  notgram_prods : grammar_constr_prod_item list list;
+}
+
+type notation_grammar = {
+  notgram_onlyprinting : bool;
+  notgram_rules : one_notation_grammar list
+}