aboutsummaryrefslogtreecommitdiff
path: root/API/API.ml
diff options
context:
space:
mode:
Diffstat (limited to 'API/API.ml')
-rw-r--r--API/API.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/API/API.ml b/API/API.ml
index 093ca97f80..32c664d7b1 100644
--- a/API/API.ml
+++ b/API/API.ml
@@ -79,6 +79,7 @@ module Nametab = Nametab
module Vernacentries = Vernacentries
module Mltop = Mltop
module Goal = Goal
+module Proof_bullet = Proof_bullet
module Proof_global = Proof_global
module Proof = Proof
module Smartlocate = Smartlocate