From fa9df2efe5666789bf91bb7761567cd53e6c451f Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 18 Dec 2016 18:14:58 +0100 Subject: [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. --- vernac/vernac.mllib | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) create mode 100644 vernac/vernac.mllib (limited to 'vernac/vernac.mllib') diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib new file mode 100644 index 000000000..94ef54f70 --- /dev/null +++ b/vernac/vernac.mllib @@ -0,0 +1,17 @@ +Lemmas +Himsg +ExplainErr +Class +Locality +Metasyntax +Auto_ind_decl +Search +Indschemes +Obligations +Command +Classes +Record +Assumptions +Vernacinterp +Mltop +Vernacentries -- cgit v1.2.3