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... --- library/library.mllib | 2 ++ 1 file changed, 2 insertions(+) (limited to 'library/library.mllib') diff --git a/library/library.mllib b/library/library.mllib index e43bfb5a1..1c0368847 100644 --- a/library/library.mllib +++ b/library/library.mllib @@ -4,7 +4,9 @@ Libobject Summary Nametab Global +Decl_kinds Lib +Misctypes Declaremods Loadpath Library -- cgit v1.2.3