From dc664b3b0c6f6f5eeba0c1092efc3f4537cdf657 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 19 Nov 2017 03:40:45 +0100 Subject: [plugins] Prepare plugin API for functional handling of state. To this purpose we allow plugins to register functions that will modify the state. This is not used yet, but will be used soon when we remove the global handling of the proof state. --- vernac/vernac.mllib | 1 + 1 file changed, 1 insertion(+) (limited to 'vernac/vernac.mllib') diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index 850902d6b..8673155e2 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -15,6 +15,7 @@ Command Classes Record Assumptions +Vernacstate Vernacinterp Mltop Topfmt -- cgit v1.2.3