From 0dc79e09b2b7c369b35191191aa257451a536540 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Sun, 11 Mar 2018 01:14:28 +0100
Subject: [api] Remove deprecated objects in engine / interp / library

---
 interp/interp.mllib | 1 -
 1 file changed, 1 deletion(-)

(limited to 'interp/interp.mllib')

diff --git a/interp/interp.mllib b/interp/interp.mllib
index 61313acc4..37a327a7d 100644
--- a/interp/interp.mllib
+++ b/interp/interp.mllib
@@ -9,7 +9,6 @@ Smartlocate
 Constrexpr_ops
 Ppextend
 Dumpglob
-Topconstr
 Reserve
 Impargs
 Implicit_quantifiers
-- 
cgit v1.2.3