From 53870b7f6890a593d1da93706f3d020a79d226e5 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 18 Sep 2018 15:22:12 +0200
Subject: [api] Remove (most) 8.9 deprecated objects.

A few of them will be of help for future cleanups. We have spared the
stuff in `Names` due to bad organization of this module following the
split from `Term`, which really difficult things removing the
constructors.
---
 dev/base_include | 1 -
 1 file changed, 1 deletion(-)

(limited to 'dev/base_include')

diff --git a/dev/base_include b/dev/base_include
index 6f54ecb241..67a7e87d78 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -99,7 +99,6 @@ open Evarutil
 open Evarsolve
 open Tacred
 open Evd
-open Universes
 open Termops
 open Namegen
 open Indrec
-- 
cgit v1.2.3