diff options
author | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-12-28 00:16:46 +0100 |
---|---|---|
committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-04-23 16:23:49 +0200 |
commit | 7dfac786626f8f6775dadc0df85360759584c976 (patch) | |
tree | 9c0355fb0dba4a48e14d0e5b316c66dfd416d685 /Makefile.common | |
parent | 5c34cfa54ec1959758baa3dd283e2e30853380db (diff) |
[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...
Diffstat (limited to 'Makefile.common')
-rw-r--r-- | Makefile.common | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common index 9a30e2a4c..eed41fbe7 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 |