From a6a7806a91275a3f509a920ee2e56f0f354a8e6c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sun, 30 Oct 2016 21:44:53 +0100
Subject: Moving Universes to the engine/ folder.

Before this patch, this module was a member of the library folder, which had
little to do with its actual use. A tiny part relative to global registering
of universe names has been effectively moved to the Global module.
---
 engine/engine.mllib | 1 +
 1 file changed, 1 insertion(+)

(limited to 'engine/engine.mllib')

diff --git a/engine/engine.mllib b/engine/engine.mllib
index 9cc6d9109..53cbbd73e 100644
--- a/engine/engine.mllib
+++ b/engine/engine.mllib
@@ -1,5 +1,6 @@
 Logic_monad
 Namegen
+Universes
 UState
 Evd
 Sigma
-- 
cgit v1.2.3