diff options
Diffstat (limited to 'API/API.ml')
| -rw-r--r-- | API/API.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/API/API.ml b/API/API.ml index f588fe193..78d9c0c26 100644 --- a/API/API.ml +++ b/API/API.ml @@ -275,6 +275,7 @@ module Command = Command module Classes = Classes (* module Record *) (* module Assumptions *) +module Vernacstate = Vernacstate module Vernacinterp = Vernacinterp module Mltop = Mltop module Topfmt = Topfmt |