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 2b7bbd561..515b152e4 100644 --- a/API/API.ml +++ b/API/API.ml @@ -138,6 +138,7 @@ module Typeclasses = Typeclasses module Pretype_errors = Pretype_errors module Notation = Notation module Declarations = Declarations +module Univops = Univops module Declareops = Declareops module Globnames = Globnames module Environ = Environ |