From 7dfac786626f8f6775dadc0df85360759584c976 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Thu, 28 Dec 2017 00:16:46 +0100
Subject: [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...
---
 dev/base_include                | 1 -
 dev/core.dbg                    | 1 -
 dev/doc/coq-src-description.txt | 6 ------
 dev/ocamldebug-coq.run          | 2 +-
 4 files changed, 1 insertion(+), 9 deletions(-)

(limited to 'dev')

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 \
-- 
cgit v1.2.3