diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2016-12-18 18:14:58 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-02-15 20:45:28 +0100 |
| commit | fa9df2efe5666789bf91bb7761567cd53e6c451f (patch) | |
| tree | dfabeded9b4060114e0f9d7f4d3760efc982ae0c /Makefile.common | |
| parent | 0df095ec0715f548180bbff70a6feb673c6726a6 (diff) | |
[stm] Break stm/toplevel dependency loop.
Currently, the STM, vernac interpretation, and the toplevel are
intertwined in a mutual dependency that needs to be resolved using
imperative callbacks.
This is problematic for a few reasons, in particular it makes the
interpretation of commands that affect the document quite intricate.
As a first step, we split the `toplevel/` directory into two: "pure"
vernac interpretation is moved to the `vernac/` directory, on which
the STM relies.
Test suite passes, and only one command seems to be disabled with this
approach, "Show Script" which is to my understanding
obsolete. Subsequent commits will fix this and refine some of the
invariants that are not needed anymore.
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 49fe1fd93..2c55d76cc 100644 --- a/Makefile.common +++ b/Makefile.common @@ -55,7 +55,7 @@ MKDIR:=install -d CORESRCDIRS:=\ config lib kernel kernel/byterun library \ proofs tactics pretyping interp stm \ - toplevel parsing printing intf engine ltac + toplevel parsing printing intf engine ltac vernac PLUGINDIRS:=\ omega romega micromega quote \ @@ -83,7 +83,7 @@ BYTERUN:=$(addprefix kernel/byterun/, \ CORECMA:=lib/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 \ + parsing/parsing.cma printing/printing.cma tactics/tactics.cma vernac/vernac.cma \ stm/stm.cma toplevel/toplevel.cma parsing/highparsing.cma ltac/ltac.cma TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma |